let W, X be set ; :: thesis:
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; :: thesis:
A3: On W = card W by A1, Th10;
defpred S₂[ 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:
A6: ex A being Ordinal st S₂[A] by A4, A5;
consider A being Ordinal such that
A7: S₂[A] and
A8: for B being Ordinal st S₂[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 S₃[ set ] means ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set such that
A12: for x being set holds
( x in LL iff ( x in On W & S₃[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 = H₂(x) ) ) from CARD_3:sch 1();
A14: LL c= On W

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

end;

A15: product ff c= Funcs LL,W

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

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

end;

hence x in Funcs LL,W by A13, A16, A17, FUNCT_2:def 2; :: thesis:

end;

let Z be set ; :: thesis:
assume Z in union LL ; :: thesis:
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 10;
A25: Y c= union LL by A24, ZFMISC_1:92;
A26: Z in Y by A23;
hence Z is Ordinal ; :: thesis:
reconsider A = Z as Ordinal by A26;
A c= Y by A23, ORDINAL1:def 2;
hence Z c= union LL by A25, XBOOLE_1:1; :: thesis:

end;

then reconsider ULL = union LL as Ordinal by ORDINAL1:31;
A27: dom (Card (id LL)) = dom (id LL) by CARD_3:def 2;
A28: dom (id LL) = LL by RELAT_1:71;

let x be set ; :: thesis:
assume A29: x in dom (Card (id LL)) ; :: thesis:
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:35;
ff . x = card (bool x) by A13, A28, A27, A29;
hence (Card (id LL)) . x in ff . x by A31, A30, CARD_1:30; :: thesis:

end;

then A32: Sum (Card (id LL)) in Product ff by A13, A28, A27, CARD_3:56;
Union (id LL) = union (rng (id LL)) by CARD_3:def 4
.= ULL by RELAT_1:71 ;
then A33: card ULL in Product ff by A32, CARD_3:54, ORDINAL1:22;
consider f being Function such that
A34: ( 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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in LL ; :: thesis:
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 5; :: thesis:

end;

then A37: card LL c= card X by A34, CARD_1:28;
card X in card W by A1, A10, Th1;
then card LL <> card W by A37, ORDINAL1:22;
then A38: not LL,W are_equipotent by CARD_1:21;
A39: card (product ff) = Product ff by CARD_3:def 8;
A40: X c= W by A2, A10, ORDINAL1:def 2;
X c= Rank (card W)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A41: x in X ; :: thesis:
then not A c= the_rank_of x by A9, CLASSES1:76, ORDINAL1:7;
then the_rank_of x in W by A8, A40, A41;
then the_rank_of x in card W by A3, ORDINAL1:def 10;
then A42: Rank (the_rank_of x) in Rank (card W) by CLASSES1:42;
x c= Rank (the_rank_of x) by CLASSES1:def 8;
hence x in Rank (card W) by A42, CLASSES1:47; :: thesis:

end;

then A43: A c= On W by A9, A3, CLASSES1:73;
On W c= ULL

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

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

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

end;

then A46: A c= succ B by A9, CLASSES1:73;
B in W by A44, ORDINAL1:def 10;
then succ B in W by A1, Th6;
hence contradiction by A1, A11, A46, CLASSES1:def 1; :: thesis:

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:76;
then the_rank_of Y in LL by A43, A12, A47;
then A49: the_rank_of Y c= ULL by ZFMISC_1:92;
B in the_rank_of Y by A48, ORDINAL1:26;
hence x in ULL by A49; :: thesis:

end;

then A50: card (On W) c= card ULL by CARD_1:27;
On W c= W by ORDINAL2:9;
then LL c= W by A14, XBOOLE_1:1;
then LL in W by A1, A38, CLASSES1:def 2;
then Funcs LL,W c= W by A1, A2, Th23;
then product ff c= W by A15, XBOOLE_1:1;
then A51: Product ff c= card W by A39, CARD_1:27;
On W = card W by A1, Th10;
hence contradiction by A33, A51, A50, CARD_1:14; :: thesis: