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 = H1(A) ) ) from A2: rng L is c=-linear
proof
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:
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 ;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum
end;
card M c= card (Rank M) by ;
then A9: M c= card (Rank M) ;
A10: Rank M = Union L by
.= 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
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;
then card (union (rng L)) c= M by ;
hence card (Rank M) = M by ; :: thesis: verum