let M be Cardinal; :: thesis: ( not M is finite implies ex A being Ordinal st M = alef A )
defpred S₁[ set ] means ( not $1 is finite implies ex A being Ordinal st $1 = alef A );
A1: S₁[ {} ] ;
A2: for K being Cardinal st S₁[K] holds
S₁[ nextcard K]

proof

let K be Cardinal; :: thesis: ( S₁[K] implies S₁[ nextcard K] )
assume that
A3: S₁[K] and
A4: not nextcard K is finite ; :: thesis: ex A being Ordinal st nextcard K = alef A

now

assume K is finite ; :: thesis: contradiction
then reconsider K' = K as finite set ;
( card K = card (card K') & card K = K ) by CARD_1:def 5;
then nextcard K = card ((card K') + 1) by NAT_1:43;
hence contradiction by A4; :: thesis: verum

end;

then consider A being Ordinal such that
A5: K = alef A by A3;
take succ A ; :: thesis: nextcard K = alef (succ A)
thus nextcard K = alef (succ A) by A5, CARD_1:39; :: thesis: verum

end;

A6: for K being Cardinal st K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S₁[N] ) holds
S₁[K]

proof

let K be Cardinal; :: thesis: ( K <> {} & K is limit_cardinal & ( for N being Cardinal st N in K holds
S₁[N] ) implies S₁[K] )
assume that
A7: ( K <> {} & K is limit_cardinal ) and
A8: for N being Cardinal st N in K holds
S₁[N] and
A9: not K is finite ; :: thesis: ex A being Ordinal st K = alef A
defpred S₂[ set ] means ex N being Cardinal st
( N = $1 & not N is finite );
consider X being set such that
A10: for x being set holds
( x in X iff ( x in K & S₂[x] ) ) from XBOOLE_0:sch 1();
defpred S₃[ set , set ] means ex A being Ordinal st
( $1 = alef A & $2 = A );
A12: for x being set st x in X holds
ex y being set st S₃[x,y]

proof

let x be set ; :: thesis: ( x in X implies ex y being set st S₃[x,y] )
assume A13: x in X ; :: thesis: ex y being set st S₃[x,y]
then consider N being Cardinal such that
A14: ( N = x & not N is finite ) by A10;
N in K by A10, A13, A14;
then ex A being Ordinal st x = alef A by A8, A14;
hence ex y being set st S₃[x,y] ; :: thesis: verum

end;

consider f being Function such that
A15: ( dom f = X & ( for x being set st x in X holds
S₃[x,f . x] ) ) from CLASSES1:sch 1(A12);

now

let x be set ; :: thesis: ( x in rng f implies ( x is Ordinal & x c= rng f ) )
assume x in rng f ; :: thesis: ( x is Ordinal & x c= rng f )
then consider y being set such that
A16: ( y in X & x = f . y ) by A15, FUNCT_1:def 5;
consider A being Ordinal such that
A17: ( y = alef A & x = A ) by A15, A16;
thus x is Ordinal by A17; :: thesis: x c= rng f
thus x c= rng f :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in rng f )
assume A18: z in x ; :: thesis: z in rng f
then reconsider z' = z as Ordinal by A17;
( alef z' in alef A & alef A in K ) by A10, A16, A17, A18, CARD_1:41;
then ( alef z' in K & not alef z' is finite ) by Th11, ORDINAL1:19;
then A19: alef z' in X by A10;
then ex A being Ordinal st
( alef z' = alef A & f . (alef z') = A ) by A15;
then z' = f . (alef z') by CARD_1:42;
hence z in rng f by A15, A19, FUNCT_1:def 5; :: thesis: verum

end;

end;

then reconsider A = rng f as Ordinal by ORDINAL1:31;
take A ; :: thesis: K = alef A
deffunc H₁( Ordinal) -> set = alef $1;
consider L being T-Sequence such that
A20: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();

now

let B be Ordinal; :: thesis: ( B in A implies succ B in A )
assume B in A ; :: thesis: succ B in A
then consider x being set such that
A21: ( x in X & B = f . x ) by A15, FUNCT_1:def 5;
consider C being Ordinal such that
A22: ( x = alef C & B = C ) by A15, A21;
( alef (succ C) = nextcard (alef C) & alef C in K ) by A10, A21, A22, CARD_1:39;
then ( alef (succ C) <> K & alef (succ C) c= K ) by A7, CARD_1:def 7, CARD_3:107;
then ( alef (succ C) in K & not alef (succ C) is finite ) by Th11, CARD_1:13;
then A23: alef (succ C) in X by A10;
then consider D being Ordinal such that
A24: ( alef (succ C) = alef D & f . (alef (succ C)) = D ) by A15;
succ C = D by A24, CARD_1:42;
hence succ B in A by A15, A22, A23, A24, FUNCT_1:def 5; :: thesis: verum

end;

then A is limit_ordinal by ORDINAL1:41;
then A25: ( A = {} or alef A = card (sup L) ) by A20, CARD_1:40;
sup L c= K

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup L or x in K )
assume A26: x in sup L ; :: thesis: x in K
then reconsider x' = x as Ordinal ;
consider C being Ordinal such that
A27: ( C in rng L & x' c= C ) by A26, ORDINAL2:29;
consider y being set such that
A28: ( y in dom L & C = L . y ) by A27, FUNCT_1:def 5;
reconsider y = y as Ordinal by A28;
A29: ( C = alef y & not alef y is finite ) by A20, A28, Th11;
consider z being set such that
A30: ( z in dom f & y = f . z ) by A20, A28, FUNCT_1:def 5;
ex D being Ordinal st
( z = alef D & y = D ) by A15, A30;
then ( C in K & K = K ) by A10, A15, A29, A30;
hence x in K by A27, ORDINAL1:22; :: thesis: verum

end;

then card (sup L) c= card K by CARD_1:27;
then A31: card (sup L) c= K by CARD_1:def 5;

now

per cases ( A = {} or A <> {} ) ;

case A = {} ; :: thesis: K = omega

then ( not omega in X & not omega is finite ) by A15, RELAT_1:65;
then not omega in K by A10;
then ( K c= omega & omega c= K ) by A9, CARD_1:14, CARD_3:102;
hence K = omega by XBOOLE_0:def 10; :: thesis: verum

end;

case A32: A <> {} ; :: thesis: not K <> alef A

assume K <> alef A ; :: thesis: contradiction
then ( card (sup L) in K & not alef A is finite ) by A25, A31, A32, Th11, CARD_1:13;
then A33: card (sup L) in X by A10, A25, A32;
then consider B being Ordinal such that
A34: ( card (sup L) = alef B & f . (card (sup L)) = B ) by A15;
A = B by A25, A32, A34, CARD_1:42;
then A in A by A15, A33, A34, FUNCT_1:def 5;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence K = alef A by CARD_1:83; :: thesis: verum

end;

for M being Cardinal holds S₁[M] from CARD_1:sch 1(A1, A2, A6);
hence ( not M is finite implies ex A being Ordinal st M = alef A ) ; :: thesis: verum