let W, X be set ; :: thesis: ( W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent implies X in Rank (card W) )
assume that
A1: W is Tarski and
A2: ( X c= Rank (card W) & not X, Rank (card W) are_equipotent ) ; :: thesis: X in Rank (card W)
A3: W <> {} by A2, CARD_1:47, CLASSES1:33;
card W = card (Rank (card W)) by A1, Th35;
then ( card X c= card W & card X <> card W ) by A2, CARD_1:21, CARD_1:27;
then A4: card X in card W by CARD_1:13;
defpred S₂[ set ] means ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set such that
A5: for x being set holds
( x in LL iff ( x in On W & S₂[x] ) ) from XBOOLE_0:sch 1();
A6: LL c= On W

proof

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

end;

now

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
A7: ( Z in Y & Y in LL ) by TARSKI:def 4;
Y in On W by A5, A7;
then reconsider Y = Y as Ordinal by ORDINAL1:def 10;
A8: Z in Y by A7;
hence Z is Ordinal ; :: thesis: Z c= union LL
reconsider A = Z as Ordinal by A8;
( A c= Y & Y c= union LL ) by A7, ORDINAL1:def 2, ZFMISC_1:92;
hence Z c= union LL by XBOOLE_1:1; :: thesis: verum

end;

then reconsider ULL = union LL as Ordinal by ORDINAL1:31;
consider f being Function such that
A9: ( 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: ( 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
A10: ( Y in X & x = the_rank_of Y ) by A5;
f . Y = x by A9, A10;
hence x in rng f by A9, A10, FUNCT_1:def 5; :: thesis: verum

end;

then card LL c= card X by A9, CARD_1:28;
then ( card LL <> card W & On W c= W ) by A4, ORDINAL1:22, ORDINAL2:9;
then A11: ( not LL,W are_equipotent & LL c= W ) by A6, CARD_1:21, XBOOLE_1:1;
then LL in W by A1, CLASSES1:def 2;
then A12: Funcs LL,W c= W by A1, A11, Th23;
A13: 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: verum

end;

consider ff being Cardinal-Function such that
A14: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H₂(x) ) ) from CARD_3:sch 1();
A15: ( 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: ( x in dom (Card (id LL)) implies (Card (id LL)) . x in ff . x )
assume x in dom (Card (id LL)) ; :: thesis: (Card (id LL)) . x in ff . x
then ( (id LL) . x = x & (Card (id LL)) . x = card ((id LL) . x) & x = x & ff . x = card (bool x) ) by A14, A15, CARD_3:def 2, FUNCT_1:35;
hence (Card (id LL)) . x in ff . x by CARD_1:30; :: thesis: verum

end;

then A16: Sum (Card (id LL)) in Product ff by A14, A15, CARD_3:56;
product ff c= Funcs LL,W

proof

let x be set ; :: 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
A17: ( 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: ( not y in rng g or y in W )
assume y in rng g ; :: thesis: y in W
then consider x being set such that
A18: ( x in dom g & y = g . x ) by FUNCT_1:def 5;
A19: ( y in ff . x & ff . x = ff . x & x = x & ff . x = card (bool x) & x in On W ) by A6, A14, A17, A18;
x in W by A6, A14, A17, A18, 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 A19; :: thesis: verum

end;

hence x in Funcs LL,W by A14, A17, FUNCT_2:def 2; :: thesis: verum

end;

then ( product ff c= W & card (product ff) = Product ff ) by A12, CARD_3:def 8, XBOOLE_1:1;
then Product ff c= card W by CARD_1:27;
then A20: card ULL in card W by A13, A16, CARD_3:54, ORDINAL1:22;
not W, {} are_equipotent by A3, CARD_1:46;
then A21: ( card W = On W & card W <> {} & card W is limit_ordinal ) by A1, Th10, Th20;
then ( union (card W) = card W & card ULL <> card W & card (card W) = card W ) by A20, ORDINAL1:def 6;
then ( ULL c= On W & ULL <> On W ) by A6, A21, ZFMISC_1:95;
then ULL c< On W by XBOOLE_0:def 8;
then ULL in card W by A21, ORDINAL1:21;
then succ ULL in card W by A21, ORDINAL1:41;
then A22: succ (succ ULL) in card W by A21, ORDINAL1:41;
X c= Rank (succ ULL)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank (succ ULL) )
assume A23: x in X ; :: thesis: x in Rank (succ ULL)
then A24: ( f . x = the_rank_of x & f . x in rng f & x = x & x in Rank (card W) ) by A2, A9, FUNCT_1:def 5;
consider A being Ordinal such that
A25: ( A in card W & x in Rank A ) by A2, A21, A23, CLASSES1:35;
defpred S₃[ Ordinal] means ( $1 in card W & x c= Rank $1 );
S₃[A] by A25, ORDINAL1:def 2;
then A26: ex A being Ordinal st S₃[A] ;
consider A being Ordinal such that
A27: S₃[A] and
A28: for B being Ordinal st S₃[B] holds
A c= B from ORDINAL1:sch 1(A26);

now

let B be Ordinal; :: thesis: ( x c= Rank B implies A c= B )
assume x c= Rank B ; :: thesis: A c= B
then ( ( A c= card W & card W c= B ) or A c= B ) by A27, A28, ORDINAL1:26;
hence A c= B by XBOOLE_1:1; :: thesis: verum

end;

then A = the_rank_of x by A27, CLASSES1:def 8;
then f . x in LL by A5, A21, A23, A24, A27;
then the_rank_of x c= ULL by A24, ZFMISC_1:92;
then ( x c= Rank (the_rank_of x) & Rank (the_rank_of x) c= Rank ULL ) by CLASSES1:43, CLASSES1:def 8;
then x c= Rank ULL by XBOOLE_1:1;
hence x in Rank (succ ULL) by CLASSES1:36; :: thesis: verum

end;

then X in Rank (succ (succ ULL)) by CLASSES1:36;
hence X in Rank (card W) by A21, A22, CLASSES1:35; :: thesis: verum