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_{1}[ Ordinal] means ( $1 in M implies card (Rank $1) in M );

A3: for B1 being Ordinal st S_{1}[B1] holds

S_{1}[ succ B1]

A7: for B1 being Ordinal st B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds

S_{1}[B2] ) holds

S_{1}[B1]
_{1}[ 0 ]
by CLASSES1:29;

for B1 being Ordinal holds S_{1}[B1]
from ORDINAL2:sch 1(A17, A3, A7);

hence card (Rank A) in M by A2; :: thesis: verum

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

A3: for B1 being Ordinal st S

S

proof

A6:
cf M = M
by A1, CARD_5:def 3;
let B1 be Ordinal; :: thesis: ( S_{1}[B1] implies S_{1}[ succ B1] )

assume A4: S_{1}[B1]
; :: thesis: S_{1}[ 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;assume A4: S

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

A7: for B1 being Ordinal st B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds

S

S

proof

A17:
S
let B1 be Ordinal; :: thesis: ( B1 <> 0 & B1 is limit_ordinal & ( for B2 being Ordinal st B2 in B1 holds

S_{1}[B2] ) implies S_{1}[B1] )

assume that

B1 <> 0 and

A8: B1 is limit_ordinal and

A9: for B2 being Ordinal st B2 in B1 holds

S_{1}[B2]
; :: thesis: S_{1}[B1]

consider L being Sequence such that

A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds

L . A = H_{1}(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

.= union (rng L) by CARD_3:def 4 ;

hence card (Rank B1) in M by A13, A14, Th33; :: thesis: verum

end;S

assume that

B1 <> 0 and

A8: B1 is limit_ordinal and

A9: for B2 being Ordinal st B2 in B1 holds

S

consider L being Sequence such that

A10: ( dom L = B1 & ( for A being Ordinal st A in B1 holds

L . A = H

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

Rank B1 =
Union L
by A8, A10, CLASSES2:24
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;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

.= union (rng L) by CARD_3:def 4 ;

hence card (Rank B1) in M by A13, A14, Th33; :: thesis: verum

for B1 being Ordinal holds S

hence card (Rank A) in M by A2; :: thesis: verum