let M be non countable Aleph; :: thesis: for A being Ordinal st M is strongly_inaccessible & A in M holds
card (Rank A) in M
let A be Ordinal; :: thesis: ( M is strongly_inaccessible & A in M implies card (Rank A) in M )
assume that
A1: M is strongly_inaccessible and
A2: A in M ; :: thesis: card (Rank A) in M
defpred S₁[ Ordinal] means ( $1 in M implies card (Rank $1) in M );
A3: for B1 being Ordinal st S₁[B1] holds
S₁[ succ B1]

proof

let B1 be Ordinal; :: thesis: ( S₁[B1] implies S₁[ succ B1] )
assume A4: S₁[B1] ; :: thesis: S₁[ succ B1]
assume succ B1 in M ; :: thesis: card (Rank (succ B1)) in M
then succ B1 c= M by ORDINAL1:def 2;
then A5: exp (2,(card (Rank B1))) in M by A1, A4, CARD_FIL:def 14, ORDINAL1:21;
Rank (succ B1) = bool (Rank B1) by CLASSES1:30;
hence card (Rank (succ B1)) in M by A5, CARD_2:31; :: thesis: verum

end;

A6: cf M = M by A1, CARD_5:def 3;
A7: for B1 being Ordinal st B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S₁[B2] ) holds
S₁[B1]

proof

let B1 be Ordinal; :: thesis: ( B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S₁[B2] ) implies S₁[B1] )
assume that
B1 <> 0 and
A8: B1 is limit_ordinal and
A9: for B2 being Ordinal st B2 in B1 holds
S₁[B2] ; :: thesis: S₁[B1]
consider L being Sequence such that
A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds
L . A = H₁(A) ) ) from ORDINAL2:sch 2();
A11: card (rng L) c= card B1 by A10, CARD_1:12;
assume A12: B1 in M ; :: thesis: card (Rank B1) in M
then card B1 in M by CARD_1:9;
then A13: card (rng L) in cf M by A6, A11, ORDINAL1:12;
A14: for Y being set st Y in rng L holds
card Y in M

proof

let Y be set ; :: thesis: ( Y in rng L implies card Y in M )
assume Y in rng L ; :: thesis: card Y in M
then consider x being object such that
A15: x in dom L and
A16: Y = L . x by FUNCT_1:def 3;
reconsider x1 = x as Element of B1 by A10, A15;
( x1 in M & Y = Rank x1 ) by A12, A10, A15, A16, ORDINAL1:10;
hence card Y in M by A9, A10, A15; :: thesis: verum

end;

Rank B1 = Union L by A8, A10, CLASSES2:24
.= union (rng L) by CARD_3:def 4 ;
hence card (Rank B1) in M by A13, A14, Th33; :: thesis: verum

end;

A17: S₁[ 0 ] by CLASSES1:29;
for B1 being Ordinal holds S₁[B1] from ORDINAL2:sch 1(A17, A3, A7);
hence card (Rank A) in M by A2; :: thesis: verum