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 S1[ Ordinal] means ( \$1 in M implies card (Rank \$1) in M );
A3: for B1 being Ordinal st S1[B1] holds
S1[ succ B1]
proof
let B1 be Ordinal; :: thesis: ( S1[B1] implies S1[ succ B1] )
assume A4: S1[B1] ; :: thesis: S1[ 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 ;
Rank (succ B1) = bool (Rank B1) by CLASSES1:30;
hence card (Rank (succ B1)) in M by ; :: thesis: verum
end;
A6: cf M = M by ;
A7: for B1 being Ordinal st B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S1[B2] ) holds
S1[B1]
proof
let B1 be Ordinal; :: thesis: ( B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds
S1[B2] ) implies S1[B1] )

assume that
B1 <> 0 and
A8: B1 is limit_ordinal and
A9: for B2 being Ordinal st B2 in B1 holds
S1[B2] ; :: thesis: S1[B1]
consider L being Sequence such that
A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds
L . A = H1(A) ) ) from A11: card (rng L) c= card B1 by ;
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 ;
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 ;
( x1 in M & Y = Rank x1 ) by ;
hence card Y in M by A9, A10, A15; :: thesis: verum
end;
Rank B1 = Union L by
.= union (rng L) by CARD_3:def 4 ;
hence card (Rank B1) in M by ; :: thesis: verum
end;
A17: S1[ 0 ] by CLASSES1:29;
for B1 being Ordinal holds S1[B1] from hence card (Rank A) in M by A2; :: thesis: verum