let W, X be set ; :: thesis:
assume A1: ( W is Tarski & W is epsilon-transitive ) ; :: thesis:
then A2: W is subset-closed ;
defpred S₂[ Ordinal] means ex X being set st
( $1 = the_rank_of X & X in W & not $1 in W );
assume ( X in W & not the_rank_of X in W ) ; :: thesis:
then A3: ex A being Ordinal st S₂[A] ;
consider A being Ordinal such that
A4: S₂[A] and
A5: for B being Ordinal st S₂[B] holds
A c= B from ORDINAL1:sch 1(A3);
consider X being set such that
A6: ( A = the_rank_of X & X in W & not A in W ) by A4;
A7: ( On W = card W & X c= W ) by A1, A6, Th10, ORDINAL1:def 2;
A8: On W = A

proof

not A in On W by A6, ORDINAL1:def 10;
hence On W c= A by A7, ORDINAL1:26; :: according to XBOOLE_0:def 10 :: thesis:
X c= Rank (card W)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then ( x in W & not A c= the_rank_of x ) by A6, A7, CLASSES1:76, ORDINAL1:7;
then the_rank_of x in W by A5;
then the_rank_of x in card W by A7, ORDINAL1:def 10;
then ( x c= Rank (the_rank_of x) & Rank (the_rank_of x) in Rank (card W) ) by CLASSES1:42, CLASSES1:def 8;
hence x in Rank (card W) by CLASSES1:47; :: thesis:

end;

hence A c= On W by A6, A7, CLASSES1:73; :: thesis:

end;

A9: card X in card W by A2, A6, Th1;
defpred S₃[ set ] means ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set such that
A10: for x being set holds
( x in LL iff ( x in On W & S₃[x] ) ) from XBOOLE_0:sch 1();
A11: LL c= On W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in LL or x in On W ) by A10; :: thesis:

end;

now

let Z be set ; :: thesis:
assume Z in union LL ; :: thesis:
then consider Y being set such that
A12: ( Z in Y & Y in LL ) by TARSKI:def 4;
Y in On W by A10, A12;
then reconsider Y = Y as Ordinal by ORDINAL1:def 10;
A13: Z in Y by A12;
hence Z is Ordinal ; :: thesis:
reconsider A = Z as Ordinal by A13;
( A c= Y & Y c= union LL ) by A12, ORDINAL1:def 2, ZFMISC_1:92;
hence Z c= union LL by XBOOLE_1:1; :: thesis:

end;

then reconsider ULL = union LL as Ordinal by ORDINAL1:31;
consider f being Function such that
A14: ( dom f = X & ( for x being set st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
LL c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in LL ; :: thesis:
then consider Y being set such that
A15: ( Y in X & x = the_rank_of Y ) by A10;
f . Y = x by A14, A15;
hence x in rng f by A14, A15, FUNCT_1:def 5; :: thesis:

end;

then card LL c= card X by A14, CARD_1:28;
then ( card LL <> card W & On W c= W ) by A9, ORDINAL1:22, ORDINAL2:9;
then ( not LL,W are_equipotent & LL c= W ) by A11, CARD_1:21, XBOOLE_1:1;
then LL in W by A1, CLASSES1:def 2;
then A16: Funcs LL,W c= W by A1, Th23;
A17: ULL = Union (id LL)

proof

Union (id LL) = union (rng (id LL)) by CARD_3:def 4
.= ULL by RELAT_1:71 ;
hence ULL = Union (id LL) ; :: thesis:

end;

consider ff being Cardinal-Function such that
A18: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H₂(x) ) ) from CARD_3:sch 1();
A19: ( dom (id LL) = LL & dom (Card (id LL)) = dom (id LL) ) by CARD_3:def 2, RELAT_1:71;

now

let x be set ; :: thesis:
assume x in dom (Card (id LL)) ; :: thesis:
then ( (id LL) . x = x & (Card (id LL)) . x = card ((id LL) . x) & x = x & ff . x = card (bool x) ) by A18, A19, CARD_3:def 2, FUNCT_1:35;
hence (Card (id LL)) . x in ff . x by CARD_1:30; :: thesis:

end;

then Sum (Card (id LL)) in Product ff by A18, A19, CARD_3:56;
then A20: card ULL in Product ff by A17, CARD_3:54, ORDINAL1:22;
product ff c= Funcs LL,W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product ff ; :: thesis:
then consider g being Function such that
A21: ( x = g & dom g = dom ff & ( for x being set st x in dom ff holds
g . x in ff . x ) ) by CARD_3:def 5;
rng g c= W

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider x being set such that
A22: ( x in dom g & y = g . x ) by FUNCT_1:def 5;
A23: ( y in ff . x & ff . x = ff . x & x = x & ff . x = card (bool x) & x in On W ) by A11, A18, A21, A22;
x in W by A11, A18, A21, A22, ORDINAL1:def 10;
then bool x in W by A1, CLASSES1:def 2;
then card (bool x) in W by A1, Th12;
then card (bool x) c= W by A1, Th6;
hence y in W by A23; :: thesis:

end;

hence x in Funcs LL,W by A18, A21, FUNCT_2:def 2; :: thesis:

end;

then ( product ff c= W & card (product ff) = Product ff ) by A16, CARD_3:def 8, XBOOLE_1:1;
then A24: Product ff c= card W by CARD_1:27;
On W c= ULL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in On W ; :: thesis:
then reconsider B = x as Ordinal by ORDINAL1:def 10;

now

assume A26: for Y being set st Y in X holds
the_rank_of Y c= B ; :: thesis:
X c= Rank (succ B)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in X ; :: thesis:
then the_rank_of y c= B by A26;
then the_rank_of y in succ B by ORDINAL1:34;
hence y in Rank (succ B) by CLASSES1:74; :: thesis:

end;

then ( A c= succ B & B in W ) by A6, A25, CLASSES1:73, ORDINAL1:def 10;
then ( A c= succ B & succ B in W ) by A1, Th6;
hence contradiction by A2, A6, CLASSES1:def 1; :: thesis:

end;

then consider Y being set such that
A27: ( Y in X & not the_rank_of Y c= B ) ;
the_rank_of Y in A by A6, A27, CLASSES1:76;
then the_rank_of Y in LL by A8, A10, A27;
then ( B in the_rank_of Y & the_rank_of Y c= ULL ) by A27, ORDINAL1:26, ZFMISC_1:92;
hence x in ULL ; :: thesis:

end;

then ( card (On W) c= card ULL & On W = card W & card W = card (card W) ) by A1, Th10, CARD_1:27;
hence contradiction by A20, A24, CARD_1:14; :: thesis: