let M be Cardinal; :: thesis: ( M is infinite implies ex A being Ordinal st M = aleph A )
defpred S₁[ set ] means ( $1 is infinite implies ex A being Ordinal st $1 = aleph A );
A1: 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
A2: S₁[K] and
A3: not nextcard K is finite ; :: thesis: ex A being Ordinal st nextcard K = aleph A

now :: thesis: not K is finite

assume K is finite ; :: thesis: contradiction
then reconsider K9 = K as finite set ;
nextcard (Segm (card K9)) = card (Segm ((card K9) + 1)) by NAT_1:42;
hence contradiction by A3; :: thesis: verum

end;

then consider A being Ordinal such that
A4: K = aleph A by A2;
take succ A ; :: thesis: nextcard K = aleph (succ A)
thus nextcard K = aleph (succ A) by A4, CARD_1:19; :: thesis: verum

end;

A5: 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] )
deffunc H₁( Ordinal) -> set = aleph $1;
defpred S₂[ object , object ] means ex A being Ordinal st
( $1 = aleph A & $2 = A );
assume that
K <> {} and
A6: K is limit_cardinal and
A7: for N being Cardinal st N in K holds
S₁[N] and
A8: not K is finite ; :: thesis: ex A being Ordinal st K = aleph A
defpred S₃[ object ] means ex N being Cardinal st
( N = $1 & not N is finite );
consider X being set such that
A9: for x being object holds
( x in X iff ( x in K & S₃[x] ) ) from XBOOLE_0:sch 1();
A10: for x being object st x in X holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis: ( x in X implies ex y being object st S₂[x,y] )
assume A11: x in X ; :: thesis: ex y being object st S₂[x,y]
then consider N being Cardinal such that
A12: N = x and
A13: not N is finite by A9;
N in K by A9, A11, A12;
then ex A being Ordinal st x = aleph A by A7, A12, A13;
hence ex y being object st S₂[x,y] ; :: thesis: verum

end;

consider f being Function such that
A14: ( dom f = X & ( for x being object st x in X holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A10);

now :: thesis: for x being set st x in rng f holds
( x is Ordinal & x c= rng f )

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 object such that
A15: y in X and
A16: x = f . y by A14, FUNCT_1:def 3;
consider A being Ordinal such that
A17: y = aleph A and
A18: x = A by A14, A15, A16;
thus x is Ordinal by A18; :: thesis: x c= rng f
thus x c= rng f :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in rng f )
assume A19: z in x ; :: thesis: z in rng f
then reconsider z9 = z as Ordinal by A18;
A20: aleph z9 in aleph A by A18, A19, CARD_1:21;
aleph A in K by A9, A15, A17;
then A21: aleph z9 in K by A20, ORDINAL1:10;
not aleph z9 is finite by Th3;
then A22: aleph z9 in X by A9, A21;
then ex A being Ordinal st
( aleph z9 = aleph A & f . (aleph z9) = A ) by A14;
then z9 = f . (aleph z9) by CARD_1:22;
hence z in rng f by A14, A22, FUNCT_1:def 3; :: thesis: verum

end;

end;

then reconsider A = rng f as epsilon-transitive epsilon-connected set by ORDINAL1:19;
consider L being Sequence such that
A23: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();

now :: thesis: for B being Ordinal st B in A holds
succ B in A

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 object such that
A24: x in X and
A25: B = f . x by A14, FUNCT_1:def 3;
consider C being Ordinal such that
A26: x = aleph C and
A27: B = C by A14, A24, A25;
A28: aleph (succ C) = nextcard (aleph C) by CARD_1:19;
aleph C in K by A9, A24, A26;
then A29: aleph (succ C) c= K by A28, CARD_3:90;
aleph (succ C) <> K by A6, A28;
then A30: aleph (succ C) in K by A29, CARD_1:3;
not aleph (succ C) is finite by Th3;
then A31: aleph (succ C) in X by A9, A30;
then consider D being Ordinal such that
A32: aleph (succ C) = aleph D and
A33: f . (aleph (succ C)) = D by A14;
succ C = D by A32, CARD_1:22;
hence succ B in A by A14, A27, A31, A33, FUNCT_1:def 3; :: thesis: verum

end;

then A is limit_ordinal by ORDINAL1:28;
then A34: ( A = {} or aleph A = card (sup L) ) by A23, CARD_1:20;
take A ; :: thesis: K = aleph A
sup L c= K

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in sup L or x in K )
assume A35: x in sup L ; :: thesis: x in K
reconsider x9 = x as Ordinal ;
consider C being Ordinal such that
A36: C in rng L and
A37: x9 c= C by A35, ORDINAL2:21;
consider y being object such that
A38: y in dom L and
A39: C = L . y by A36, FUNCT_1:def 3;
reconsider y = y as Ordinal by A38;
A40: C = aleph y by A23, A38, A39;
consider z being object such that
A41: z in dom f and
A42: y = f . z by A23, A38, FUNCT_1:def 3;
ex D being Ordinal st
( z = aleph D & y = D ) by A14, A41, A42;
then C in K by A9, A14, A40, A41;
hence x in K by A37, ORDINAL1:12; :: thesis: verum

end;

then card (sup L) c= card K by CARD_1:11;
then A43: card (sup L) c= K ;

now :: thesis: ( ( A = {} & K = omega ) or ( A <> {} & not K <> aleph A ) )

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

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

then not omega in X by A14, RELAT_1:42;
then not omega in K by A9;
then A44: K c= omega by CARD_1:4;
omega c= K by A8, CARD_3:85;
hence K = omega by A44; :: thesis: verum

end;

case A45: A <> {} ; :: thesis: not K <> aleph A

assume K <> aleph A ; :: thesis: contradiction
then A46: card (sup L) in K by A34, A43, A45, CARD_1:3;
not aleph A is finite by Th3;
then A47: card (sup L) in X by A9, A34, A45, A46;
then consider B being Ordinal such that
A48: card (sup L) = aleph B and
A49: f . (card (sup L)) = B by A14;
A = B by A34, A45, A48, CARD_1:22;
then A in A by A14, A47, A49, FUNCT_1:def 3;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence K = aleph A by CARD_1:46; :: thesis: verum

end;

A50: S₁[ {} ] ;
for M being Cardinal holds S₁[M] from CARD_1:sch 1(A50, A1, A5);
hence ( M is infinite implies ex A being Ordinal st M = aleph A ) ; :: thesis: verum