let X, W 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) and
A3: not X, Rank (card W) are_equipotent ; :: thesis: X in Rank (card W)
defpred S₂[ object ] means ex Y being set st
( Y in X & $1 = the_rank_of Y );
consider LL being set such that
A4: for x being object holds
( x in LL iff ( x in On W & S₂[x] ) ) from XBOOLE_0:sch 1();
consider ff being Cardinal-Function such that
A5: ( dom ff = LL & ( for x being set st x in LL holds
ff . x = H₂(x) ) ) from CARD_3:sch 1();
A6: LL c= On W by A4;
A7: 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
A8: x = g and
A9: dom g = dom ff and
A10: 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
A11: x in dom g and
A12: y = g . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
A13: ff . x = card (bool x) by A5, A9, A11;
x in W by A6, A5, A9, A11, ORDINAL1:def 9;
then bool x in W by A1;
then card (bool x) in W by A1, Th11;
then A14: card (bool x) c= W by A1, Th5;
y in ff . x by A9, A10, A11, A12;
hence y in W by A13, A14; :: thesis: verum

end;

hence x in Funcs (LL,W) by A5, A8, A9, FUNCT_2:def 2; :: thesis: verum

end;

A15: card W = card (Rank (card W)) by A1, Th34;
then A16: card X <> card W by A3, CARD_1:5;
On W c= W by ORDINAL2:7;
then A17: LL c= W by A6;

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
A18: Z in Y and
A19: Y in LL by TARSKI:def 4;
Y in On W by A4, A19;
then reconsider Y = Y as Ordinal by ORDINAL1:def 9;
A20: Y c= union LL by A19, ZFMISC_1:74;
A21: Z in Y by A18;
hence Z is Ordinal ; :: thesis: Z c= union LL
reconsider A = Z as Ordinal by A21;
A c= Y by A18, ORDINAL1:def 2;
hence Z c= union LL by A20; :: thesis: verum

end;

then reconsider ULL = union LL as epsilon-transitive epsilon-connected set by ORDINAL1:19;
A22: dom (Card (id LL)) = dom (id LL) by CARD_3:def 2;
A23: 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 A24: x in dom (Card (id LL)) ; :: thesis: (Card (id LL)) . x in ff . x
then A25: (Card (id LL)) . x = card ((id LL) . x) by A22, CARD_3:def 2;
A26: (id LL) . x = x by A23, A22, A24, FUNCT_1:18;
reconsider xx = x as set by TARSKI:1;
ff . x = card (bool xx) by A5, A23, A22, A24;
hence (Card (id LL)) . x in ff . x by A26, A25, CARD_1:14; :: thesis: verum

end;

then A27: Sum (Card (id LL)) in Product ff by A5, A23, A22, CARD_3:41;
consider f being Function such that
A28: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(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
A29: Y in X and
A30: x = the_rank_of Y by A4;
f . Y = x by A28, A29, A30;
hence x in rng f by A28, A29, FUNCT_1:def 3; :: thesis: verum

end;

then A31: card LL c= card X by A28, CARD_1:12;
A32: card (product ff) = Product ff by CARD_3:def 8;
card X c= card W by A2, A15, CARD_1:11;
then card X in card W by A16, CARD_1:3;
then card LL <> card W by A31, ORDINAL1:12;
then not LL,W are_equipotent by CARD_1:5;
then LL in W by A1, A17;
then Funcs (LL,W) c= W by A1, A17, Th22;
then product ff c= W by A7;
then A33: Product ff c= card W by A32, CARD_1:11;
A34: card W is limit_ordinal by A1, Th19;
A35: card W = On W by A1, Th9;
X c= Rank (succ ULL)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank (succ ULL) )
reconsider xx = x as set by TARSKI:1;
defpred S₃[ Ordinal] means ( $1 in card W & xx c= Rank $1 );
assume A36: x in X ; :: thesis: x in Rank (succ ULL)
then A37: f . x = the_rank_of xx by A28;
consider A being Ordinal such that
A38: A in card W and
A39: x in Rank A by A2, A34, A36, CLASSES1:29, CLASSES1:31;
S₃[A] by A38, A39, ORDINAL1:def 2;
then A40: ex A being Ordinal st S₃[A] ;
consider A being Ordinal such that
A41: S₃[A] and
A42: for B being Ordinal st S₃[B] holds
A c= B from ORDINAL1:sch 1(A40);

now :: thesis: for B being Ordinal st xx c= Rank B holds
A c= B

let B be Ordinal; :: thesis: ( xx c= Rank B implies A c= B )
assume xx c= Rank B ; :: thesis: A c= B
then ( ( A c= card W & card W c= B ) or A c= B ) by A41, A42, ORDINAL1:16;
hence A c= B ; :: thesis: verum

end;

then A = the_rank_of xx by A41, CLASSES1:def 9;
then f . x in LL by A4, A35, A36, A37, A41;
then the_rank_of xx c= ULL by A37, ZFMISC_1:74;
then A43: Rank (the_rank_of xx) c= Rank ULL by CLASSES1:37;
xx c= Rank (the_rank_of xx) by CLASSES1:def 9;
then xx c= Rank ULL by A43;
hence x in Rank (succ ULL) by CLASSES1:32; :: thesis: verum

end;

then A44: X in Rank (succ (succ ULL)) by CLASSES1:32;
Union (id LL) = union (rng (id LL)) by CARD_3:def 4
.= ULL by RELAT_1:45 ;
then card ULL in card W by A27, A33, CARD_3:39, ORDINAL1:12;
then A45: ULL <> On W by A35;
union (card W) = card W by A34;
then ULL c= On W by A6, A35, ZFMISC_1:77;
then ULL c< On W by A45;
then ULL in card W by A35, ORDINAL1:11;
then succ ULL in card W by A34, ORDINAL1:28;
then succ (succ ULL) in card W by A34, ORDINAL1:28;
hence X in Rank (card W) by A34, A44, CLASSES1:31; :: thesis: verum