let X, W be set ; :: thesis: ( W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W )
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; :: thesis: ( not X in W or the_rank_of X in W )
A3: On W = card W by A1, Th9;
defpred S2[ Ordinal] means ex X being set st
( $1 = the_rank_of X & X in W & not $1 in W );
assume that
A4: X in W and
A5: not the_rank_of X in W ; :: thesis: contradiction
A6: ex A being Ordinal st S2[A] by A4, A5;
consider A being Ordinal such that
A7: S2[A] and
A8: for B being Ordinal st S2[B] holds
A c= B from ORDINAL1:sch 1(A6);
 consider X being set such that
A9: A = the_rank_of X and
A10: X in W and
A11: not A in W by A7;
defpred S3[ object ] means ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set such that
A12: for x being object holds
( x in LL iff ( x in On W & S3[x] ) ) from XBOOLE_0:sch 1();
 consider ff being Cardinal-Function such that
A13: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H2(x) ) ) from CARD_3:sch 1();
 A14: LL c= On W by A12;
A15: product ff c= Funcs (LL,W)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product ff or x in Funcs (LL,W) )
assume x in product ff ; :: thesis: x in Funcs (LL,W)
then consider g being Function such that
A16: x = g and
A17: dom g = dom ff and
A18: for x being object st x in dom ff holds
g . x in ff . x by CARD_3:def 5;
rng g c= W
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in W )
assume y in rng g ; :: thesis: y in W
then consider x being object such that
A19: x in dom g and
A20: y = g . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
A21: ff . x = card (bool x) by A13, A17, A19;
x in W by A14, A13, A17, A19, ORDINAL1:def 9;
then bool x in W by A1;
then card (bool x) in W by A1, Th11;
then A22: card (bool x) c= W by A1, Th5;
y in ff . x by A17, A18, A19, A20;
hence y in W by A21, A22; :: thesis: verum
end;
hence x in Funcs (LL,W) by A13, A16, A17, FUNCT_2:def 2; :: thesis: verum
end;
now :: thesis: for Z being set st Z in union LL holds
( Z is Ordinal & Z c= union LL )
let Z be set ; :: thesis: ( Z in union LL implies ( Z is Ordinal & Z c= union LL ) )
assume Z in union LL ; :: thesis: ( Z is Ordinal & Z c= union LL )
then consider Y being set such that
A23: Z in Y and
A24: Y in LL by TARSKI:def 4;
Y in On W by A12, A24;
then reconsider Y = Y as Ordinal by ORDINAL1:def 9;
A25: Y c= union LL by A24, ZFMISC_1:74;
A26: Z in Y by A23;
hence Z is Ordinal ; :: thesis: Z c= union LL
reconsider A = Z as Ordinal by A26;
A c= Y by A23, ORDINAL1:def 2;
hence Z c= union LL by A25; :: thesis: verum
end;
then reconsider ULL = union LL as epsilon-transitive epsilon-connected set by ORDINAL1:19;
A27: dom (Card (id LL)) = dom (id LL) by CARD_3:def 2;
A28: dom (id LL) = LL by RELAT_1:45;
now :: thesis: for x being object st x in dom (Card (id LL)) holds
(Card (id LL)) . x in ff . x
let x be object ; :: thesis: ( x in dom (Card (id LL)) implies (Card (id LL)) . x in ff . x )
assume A29: x in dom (Card (id LL)) ; :: thesis: (Card (id LL)) . x in ff . x
then A30: (Card (id LL)) . x = card ((id LL) . x) by A27, CARD_3:def 2;
A31: (id LL) . x = x by A28, A27, A29, FUNCT_1:18;
reconsider xx = x as set by TARSKI:1;
ff . x = card (bool xx) by A13, A28, A27, A29;
hence (Card (id LL)) . x in ff . x by A31, A30, CARD_1:14; :: thesis: verum
end;
then A32: Sum (Card (id LL)) in Product ff by A13, A28, A27, CARD_3:41;
Union (id LL) = union (rng (id LL)) by CARD_3:def 4
.= ULL by RELAT_1:45 ;
then A33: card ULL in Product ff by A32, CARD_3:39, ORDINAL1:12;
consider f being Function such that
A34: ( dom f = X & ( for x being object st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch 3();
 LL c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LL or x in rng f )
assume x in LL ; :: thesis: x in rng f
then consider Y being set such that
A35: Y in X and
A36: x = the_rank_of Y by A12;
f . Y = x by A34, A35, A36;
hence x in rng f by A34, A35, FUNCT_1:def 3; :: thesis: verum
end;
then A37: card LL c= card X by A34, CARD_1:12;
card X in card W by A1, A10, Th1;
then card LL <> card W by A37, ORDINAL1:12;
then A38: not LL,W are_equipotent by CARD_1:5;
A39: card (product ff) = Product ff by CARD_3:def 8;
A40: X c= W by A2, A10;
X c= Rank (card W)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank (card W) )
reconsider xx = x as set by TARSKI:1;
assume A41: x in X ; :: thesis: x in Rank (card W)
then not A c= the_rank_of xx by A9, CLASSES1:68, ORDINAL1:5;
then the_rank_of xx in W by A8, A40, A41;
then the_rank_of xx in card W by A3, ORDINAL1:def 9;
then A42: Rank (the_rank_of xx) in Rank (card W) by CLASSES1:36;
xx c= Rank (the_rank_of xx) by CLASSES1:def 9;
hence x in Rank (card W) by A42, CLASSES1:41; :: thesis: verum
end;
then A43: A c= On W by A9, A3, CLASSES1:65;
On W c= ULL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On W or x in ULL )
assume A44: x in On W ; :: thesis: x in ULL
then reconsider B = x as Ordinal by ORDINAL1:def 9;
now :: thesis: ex Y being set st
( Y in X & not the_rank_of Y c= B )
assume A45: for Y being set st Y in X holds
the_rank_of Y c= B ; :: thesis: contradiction
X c= Rank (succ B)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in Rank (succ B) )
reconsider yy = y as set by TARSKI:1;
assume y in X ; :: thesis: y in Rank (succ B)
then the_rank_of yy c= B by A45;
then the_rank_of yy in succ B by ORDINAL1:22;
hence y in Rank (succ B) by CLASSES1:66; :: thesis: verum
end;
then A46: A c= succ B by A9, CLASSES1:65;
B in W by A44, ORDINAL1:def 9;
then succ B in W by A1, Th5;
hence contradiction by A1, A11, A46, CLASSES1:def 1; :: thesis: verum
end;
then consider Y being set such that
A47: Y in X and
A48: not the_rank_of Y c= B ;
the_rank_of Y in A by A9, A47, CLASSES1:68;
then the_rank_of Y in LL by A43, A12, A47;
then A49: the_rank_of Y c= ULL by ZFMISC_1:74;
B in the_rank_of Y by A48, ORDINAL1:16;
hence x in ULL by A49; :: thesis: verum
end;
then A50: card (On W) c= card ULL by CARD_1:11;
On W c= W by ORDINAL2:7;
then LL c= W by A14;
then LL in W by A1, A38;
then Funcs (LL,W) c= W by A1, A2, Th22;
then product ff c= W by A15;
then A51: Product ff c= card W by A39, CARD_1:11;
On W = card W by A1, Th9;
hence contradiction by A33, A51, A50, CARD_1:4; :: thesis: verum