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

assume A1: M is strongly_inaccessible ; :: thesis: Rank M is Tarski

thus for X, Y being set st X in Rank M & Y c= X holds

Y in Rank M by CLASSES1:41; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b_{1} being set holds

( not b_{1} in Rank M or bool b_{1} in Rank M ) ) & ( for b_{1} being set holds

( not b_{1} c= Rank M or b_{1}, Rank M are_equipotent or b_{1} in Rank M ) ) )

thus for X being set st X in Rank M holds

bool X in Rank M :: thesis: for b_{1} being set holds

( not b_{1} c= Rank M or b_{1}, Rank M are_equipotent or b_{1} in Rank M )

thus for X being set holds

( not X c= Rank M or X, Rank M are_equipotent or X in Rank M ) :: thesis: verum

assume A1: M is strongly_inaccessible ; :: thesis: Rank M is Tarski

thus for X, Y being set st X in Rank M & Y c= X holds

Y in Rank M by CLASSES1:41; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b

( not b

( not b

thus for X being set st X in Rank M holds

bool X in Rank M :: thesis: for b

( not b

proof

A3:
cf M = M
by A1, CARD_5:def 3;
let X be set ; :: thesis: ( X in Rank M implies bool X in Rank M )

assume X in Rank M ; :: thesis: bool X in Rank M

then consider A being Ordinal such that

A2: ( A in M & X in Rank A ) by CLASSES1:31;

( succ A in M & bool X in Rank (succ A) ) by A2, CLASSES1:42, ORDINAL1:28;

hence bool X in Rank M by CLASSES1:31; :: thesis: verum

end;assume X in Rank M ; :: thesis: bool X in Rank M

then consider A being Ordinal such that

A2: ( A in M & X in Rank A ) by CLASSES1:31;

( succ A in M & bool X in Rank (succ A) ) by A2, CLASSES1:42, ORDINAL1:28;

hence bool X in Rank M by CLASSES1:31; :: thesis: verum

thus for X being set holds

( not X c= Rank M or X, Rank M are_equipotent or X in Rank M ) :: thesis: verum

proof

let X be set ; :: thesis: ( not X c= Rank M or X, Rank M are_equipotent or X in Rank M )

A4: ( card X c< M iff ( card X c= M & card X <> M ) ) by XBOOLE_0:def 8;

set R = the_rank_of X;

assume that

A5: X c= Rank M and

A6: not X, Rank M are_equipotent and

A7: not X in Rank M ; :: thesis: contradiction

( card X c= card (Rank M) & card X <> card (Rank M) ) by A5, A6, CARD_1:5, CARD_1:11;

then A8: card X in M by A1, A4, Th35, ORDINAL1:11;

end;A4: ( card X c< M iff ( card X c= M & card X <> M ) ) by XBOOLE_0:def 8;

set R = the_rank_of X;

assume that

A5: X c= Rank M and

A6: not X, Rank M are_equipotent and

A7: not X in Rank M ; :: thesis: contradiction

( card X c= card (Rank M) & card X <> card (Rank M) ) by A5, A6, CARD_1:5, CARD_1:11;

then A8: card X in M by A1, A4, Th35, ORDINAL1:11;

per cases
( X = {} or not X is empty )
;

end;

suppose A9:
X = {}
; :: thesis: contradiction

{} c= M
;

then {} c< M by XBOOLE_0:def 8;

then A10: {} in M by ORDINAL1:11;

M c= Rank M by CLASSES1:38;

hence contradiction by A7, A9, A10; :: thesis: verum

end;then {} c< M by XBOOLE_0:def 8;

then A10: {} in M by ORDINAL1:11;

M c= Rank M by CLASSES1:38;

hence contradiction by A7, A9, A10; :: thesis: verum

suppose
not X is empty
; :: thesis: contradiction

then reconsider X1 = X as non empty set ;

the_rank_of X in M

end;the_rank_of X in M

proof

hence
contradiction
by A7, CLASSES1:66; :: thesis: verum
deffunc H_{2}( set ) -> set = the_rank_of $1;

set RANKS = { H_{2}(x) where x is Element of X1 : x in X1 } ;

A11: for x being set st x in X holds

x in Rank M by A5;

{ H_{2}(x) where x is Element of X1 : x in X1 } c= M
_{2}(x) where x is Element of X1 : x in X1 } as Subset of M ;

ex N1 being Ordinal st

( N1 in M & ( for x being set st x in X1 holds

the_rank_of x in N1 ) )

A17: N1 in M and

A18: for x being set st x in X1 holds

the_rank_of x in N1 ;

the_rank_of X c= N1 by A18, CLASSES1:69;

hence the_rank_of X in M by A17, ORDINAL1:12; :: thesis: verum

end;set RANKS = { H

A11: for x being set st x in X holds

x in Rank M by A5;

{ H

proof

then reconsider RANKS1 = { H
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { H_{2}(x) where x is Element of X1 : x in X1 } or y in M )

assume y in { H_{2}(x) where x is Element of X1 : x in X1 }
; :: thesis: y in M

then consider x being Element of X1 such that

A12: y = the_rank_of x and

x in X1 ;

x in Rank M by A11;

hence y in M by A12, CLASSES1:66; :: thesis: verum

end;assume y in { H

then consider x being Element of X1 such that

A12: y = the_rank_of x and

x in X1 ;

x in Rank M by A11;

hence y in M by A12, CLASSES1:66; :: thesis: verum

ex N1 being Ordinal st

( N1 in M & ( for x being set st x in X1 holds

the_rank_of x in N1 ) )

proof

then consider N1 being Ordinal such that
assume A13:
for N1 being Ordinal st N1 in M holds

ex x being set st

( x in X1 & not the_rank_of x in N1 ) ; :: thesis: contradiction

for N1 being Ordinal st N1 in M holds

ex C being Ordinal st

( C in { H_{2}(x) where x is Element of X1 : x in X1 } & N1 c= C )

then A16: cf M c= card RANKS1 by Th20;

card { H_{2}(x) where x is Element of X1 : x in X1 } c= card X1
from TREES_2:sch 2();

then M c= card X1 by A3, A16;

then card X1 in card X1 by A8;

hence contradiction ; :: thesis: verum

end;ex x being set st

( x in X1 & not the_rank_of x in N1 ) ; :: thesis: contradiction

for N1 being Ordinal st N1 in M holds

ex C being Ordinal st

( C in { H

proof

then
RANKS1 is unbounded
by Th6;
let N1 be Ordinal; :: thesis: ( N1 in M implies ex C being Ordinal st

( C in { H_{2}(x) where x is Element of X1 : x in X1 } & N1 c= C ) )

assume N1 in M ; :: thesis: ex C being Ordinal st

( C in { H_{2}(x) where x is Element of X1 : x in X1 } & N1 c= C )

then consider x being set such that

A14: x in X1 and

A15: not the_rank_of x in N1 by A13;

take C = the_rank_of x; :: thesis: ( C in { H_{2}(x) where x is Element of X1 : x in X1 } & N1 c= C )

thus C in { H_{2}(x) where x is Element of X1 : x in X1 }
by A14; :: thesis: N1 c= C

thus N1 c= C by A15, ORDINAL1:16; :: thesis: verum

end;( C in { H

assume N1 in M ; :: thesis: ex C being Ordinal st

( C in { H

then consider x being set such that

A14: x in X1 and

A15: not the_rank_of x in N1 by A13;

take C = the_rank_of x; :: thesis: ( C in { H

thus C in { H

thus N1 c= C by A15, ORDINAL1:16; :: thesis: verum

then A16: cf M c= card RANKS1 by Th20;

card { H

then M c= card X1 by A3, A16;

then card X1 in card X1 by A8;

hence contradiction ; :: thesis: verum

A17: N1 in M and

A18: for x being set st x in X1 holds

the_rank_of x in N1 ;

the_rank_of X c= N1 by A18, CLASSES1:69;

hence the_rank_of X in M by A17, ORDINAL1:12; :: thesis: verum