let M be non countable Aleph; :: thesis: ( M is strongly_inaccessible implies card (Rank M) = M )

consider L being Sequence such that

A1: ( dom L = M & ( for A being Ordinal st A in M holds

L . A = H_{1}(A) ) )
from ORDINAL2:sch 2();

A2: rng L is c=-linear

then A9: M c= card (Rank M) ;

A10: Rank M = Union L by A1, CLASSES2:24

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

assume A11: M is strongly_inaccessible ; :: thesis: card (Rank M) = M

hence card (Rank M) = M by A10, A9, XBOOLE_0:def 10; :: thesis: verum

consider L being Sequence such that

A1: ( dom L = M & ( for A being Ordinal st A in M holds

L . A = H

A2: rng L is c=-linear

proof

card M c= card (Rank M)
by CARD_1:11, CLASSES1:38;
let X, Y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not X in rng L or not Y in rng L or X,Y are_c=-comparable )

assume X in rng L ; :: thesis: ( not Y in rng L or X,Y are_c=-comparable )

then consider x being object such that

A3: x in dom L and

A4: X = L . x by FUNCT_1:def 3;

assume Y in rng L ; :: thesis: X,Y are_c=-comparable

then consider y being object such that

A5: y in dom L and

A6: Y = L . y by FUNCT_1:def 3;

reconsider x = x, y = y as Ordinal by A3, A5;

A7: Y = Rank y by A1, A5, A6;

A8: ( x c= y or y c= x ) ;

X = Rank x by A1, A3, A4;

then ( X c= Y or Y c= X ) by A7, A8, CLASSES1:37;

hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;assume X in rng L ; :: thesis: ( not Y in rng L or X,Y are_c=-comparable )

then consider x being object such that

A3: x in dom L and

A4: X = L . x by FUNCT_1:def 3;

assume Y in rng L ; :: thesis: X,Y are_c=-comparable

then consider y being object such that

A5: y in dom L and

A6: Y = L . y by FUNCT_1:def 3;

reconsider x = x, y = y as Ordinal by A3, A5;

A7: Y = Rank y by A1, A5, A6;

A8: ( x c= y or y c= x ) ;

X = Rank x by A1, A3, A4;

then ( X c= Y or Y c= X ) by A7, A8, CLASSES1:37;

hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

then A9: M c= card (Rank M) ;

A10: Rank M = Union L by A1, CLASSES2:24

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

assume A11: M is strongly_inaccessible ; :: thesis: card (Rank M) = M

now :: thesis: for X being set st X in rng L holds

card X in M

then
card (union (rng L)) c= M
by A2, CARD_3:46;card X in M

let X be set ; :: thesis: ( X in rng L implies card X in M )

assume X in rng L ; :: thesis: card X in M

then consider x being object such that

A12: x in dom L and

A13: X = L . x by FUNCT_1:def 3;

reconsider x = x as Ordinal by A12;

card (Rank x) in M by A11, A1, A12, Th34;

hence card X in M by A1, A12, A13; :: thesis: verum

end;assume X in rng L ; :: thesis: card X in M

then consider x being object such that

A12: x in dom L and

A13: X = L . x by FUNCT_1:def 3;

reconsider x = x as Ordinal by A12;

card (Rank x) in M by A11, A1, A12, Th34;

hence card X in M by A1, A12, A13; :: thesis: verum

hence card (Rank M) = M by A10, A9, XBOOLE_0:def 10; :: thesis: verum