:: Mahlo and inaccessible cardinals
:: by Josef Urban
::
:: Received August 28, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


:: ::
:: Some initial settings ::
:: ::
registration
cluster ordinal infinite cardinal -> limit_ordinal for set ;
coherence
for b1 being Ordinal st b1 is cardinal & b1 is infinite holds
b1 is limit_ordinal ;
end;

registration
cluster ordinal limit_ordinal non empty -> infinite for set ;
coherence
for b1 being Ordinal st not b1 is empty & b1 is limit_ordinal holds
b1 is infinite
proof end;
end;

registration
cluster non finite cardinal non limit_cardinal -> non countable for set ;
coherence
for b1 being Aleph st not b1 is limit_cardinal holds
not b1 is countable
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable regular for set ;
existence
ex b1 being Aleph st
( b1 is regular & not b1 is countable )
proof end;
end;

definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
pred X is_unbounded_in A means :: CARD_LAR:def 1
( X c= A & sup X = A );
pred X is_closed_in A means :: CARD_LAR:def 2
( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) );
end;

:: deftheorem defines is_unbounded_in CARD_LAR:def 1 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_unbounded_in A iff ( X c= A & sup X = A ) );

:: deftheorem defines is_closed_in CARD_LAR:def 2 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_closed_in A iff ( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) ) );

definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
pred X is_club_in A means :: CARD_LAR:def 3
( X is_closed_in A & X is_unbounded_in A );
end;

:: deftheorem defines is_club_in CARD_LAR:def 3 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_club_in A iff ( X is_closed_in A & X is_unbounded_in A ) );

definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X is unbounded means :: CARD_LAR:def 4
 sup X = A;
attr X is closed means :: CARD_LAR:def 5
 for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X;
end;

:: deftheorem defines unbounded CARD_LAR:def 4 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff sup X = A );

:: deftheorem defines closed CARD_LAR:def 5 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is closed iff for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X );

notation
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
antonym bounded X for unbounded ;
end;

theorem Th1: :: CARD_LAR:1
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
proof end;

:: should be probably in ordinal2
theorem Th2: :: CARD_LAR:2
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds X c= sup X by ORDINAL2:19;

theorem Th3: :: CARD_LAR:3
for A being limit_ordinal infinite Ordinal
for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) holds
sup X is limit_ordinal infinite Ordinal
proof end;

theorem Th4: :: CARD_LAR:4
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is bounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
proof end;

theorem Th5: :: CARD_LAR:5
for A, B being limit_ordinal infinite Ordinal
for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
proof end;

theorem Th6: :: CARD_LAR:6
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )
proof end;

theorem Th7: :: CARD_LAR:7
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded holds
not X is empty
proof end;

theorem Th8: :: CARD_LAR:8
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
proof end;

definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
let B1 be Ordinal;
assume A1: X is unbounded ;
assume A2: B1 in A ;
func LBound (B1,X) -> Element of X equals :Def6: :: CARD_LAR:def 6
 inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;
coherence
inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } is Element of X
proof end;
end;

:: deftheorem Def6 defines LBound CARD_LAR:def 6 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A
for B1 being Ordinal st X is unbounded & B1 in A holds
LBound (B1,X) = inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;

theorem Th9: :: CARD_LAR:9
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound (B1,X) in X & B1 in LBound (B1,X) )
proof end;

theorem Th10: :: CARD_LAR:10
for A being limit_ordinal infinite Ordinal holds
( [#] A is closed & [#] A is unbounded ) by ORDINAL2:18;

theorem Th11: :: CARD_LAR:11
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st B1 in A & X is closed & X is unbounded holds
( X \ B1 is closed & X \ B1 is unbounded )
proof end;

theorem Th12: :: CARD_LAR:12
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal st B1 in A holds
( A \ B1 is closed & A \ B1 is unbounded )
proof end;

definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X is stationary means :: CARD_LAR:def 7
 for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ;
end;

:: deftheorem defines stationary CARD_LAR:def 7 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is stationary iff for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty );

theorem Th13: :: CARD_LAR:13
for A being limit_ordinal infinite Ordinal
for X, Y being Subset of A st X is stationary & X c= Y holds
Y is stationary
proof end;

definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
pred X is_stationary_in A means :: CARD_LAR:def 8
( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) );
end;

:: deftheorem defines is_stationary_in CARD_LAR:def 8 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_stationary_in A iff ( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) ) );

theorem Th14: :: CARD_LAR:14
for A being limit_ordinal infinite Ordinal
for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds
Y is_stationary_in A
proof end;

:: belongs e.g. to setfam?
definition
let X be set ;
let S be Subset-Family of X;
:: original: Element
redefine mode Element of S -> Subset of X;
coherence
for b1 being Element of S holds b1 is Subset of X
proof end;
end;

theorem :: CARD_LAR:15
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is stationary holds
X is unbounded
proof end;

definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
func limpoints X -> Subset of A equals :: CARD_LAR:def 9
 { B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;
coherence
{ B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } is Subset of A
proof end;
end;

:: deftheorem defines limpoints CARD_LAR:def 9 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X = { B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;

theorem Th16: :: CARD_LAR:16
for A being limit_ordinal infinite Ordinal
for B1, B3 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
proof end;

theorem :: CARD_LAR:17
for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X c= B1 holds
limpoints X c= succ B1
proof end;

theorem Th18: :: CARD_LAR:18
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X is closed
proof end;

:: mainly used for MahloReg, LimUnb says this usually doesnot happen
theorem Th19: :: CARD_LAR:19
for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded & limpoints X is bounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
proof end;

registration
let M be non countable Aleph;
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal for Element of M;
existence
ex b1 being Element of M st
( b1 is cardinal & b1 is infinite )
proof end;
end;

theorem Th20: :: CARD_LAR:20
for M being Aleph
for X being Subset of M st X is unbounded holds
cf M c= card X
proof end;

theorem Th21: :: CARD_LAR:21
for M being non countable Aleph
for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds
meet S is closed
proof end;

theorem Th22: :: CARD_LAR:22
for M being non countable Aleph
for X being Subset of M st omega in cf M holds
for f being sequence of X holds sup (rng f) in M
proof end;

theorem :: CARD_LAR:23
for M being non countable Aleph st omega in cf M holds
for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )
proof end;

theorem Th24: :: CARD_LAR:24
for M being non countable Aleph
for X being Subset of M st omega in cf M & X is unbounded holds
for B1 being Ordinal st B1 in M holds
ex B being limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )
proof end;

theorem :: CARD_LAR:25
for M being non countable Aleph
for X being Subset of M st omega in cf M & X is unbounded holds
limpoints X is unbounded
proof end;

definition
let M be non countable Aleph;
attr M is Mahlo means :: CARD_LAR:def 10
 { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M;
attr M is strongly_Mahlo means :: CARD_LAR:def 11
 { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M;
end;

:: deftheorem defines Mahlo CARD_LAR:def 10 :
for M being non countable Aleph holds
( M is Mahlo iff { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M );

:: deftheorem defines strongly_Mahlo CARD_LAR:def 11 :
for M being non countable Aleph holds
( M is strongly_Mahlo iff { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M );

theorem Th26: :: CARD_LAR:26
for M being non countable Aleph st M is strongly_Mahlo holds
M is Mahlo
proof end;

theorem Th27: :: CARD_LAR:27
for M being non countable Aleph st M is Mahlo holds
M is regular
proof end;

theorem Th28: :: CARD_LAR:28
for M being non countable Aleph st M is Mahlo holds
M is limit_cardinal
proof end;

theorem :: CARD_LAR:29
for M being non countable Aleph st M is Mahlo holds
M is inaccessible
proof end;

theorem Th30: :: CARD_LAR:30
for M being non countable Aleph st M is strongly_Mahlo holds
M is strong_limit
proof end;

theorem :: CARD_LAR:31
for M being non countable Aleph st M is strongly_Mahlo holds
M is strongly_inaccessible
proof end;

:: shouldnot be e.g. in CARD_1? or is there st. more general?
theorem Th32: :: CARD_LAR:32
for X being set st ( for x being set st x in X holds
ex y being set st
( y in X & x c= y & y is Cardinal ) ) holds
union X is Cardinal
proof end;

theorem Th33: :: CARD_LAR:33
for X being set
for M being Aleph st card X in cf M & ( for Y being set st Y in X holds
card Y in M ) holds
card (union X) in M
proof end;

deffunc H1( Ordinal) -> set = Rank $1;

theorem Th34: :: CARD_LAR:34
for M being non countable Aleph
for A being Ordinal st M is strongly_inaccessible & A in M holds
card (Rank A) in M
proof end;

theorem Th35: :: CARD_LAR:35
for M being non countable Aleph st M is strongly_inaccessible holds
card (Rank M) = M
proof end;

theorem Th36: :: CARD_LAR:36
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Tarski
proof end;

theorem Th37: :: CARD_LAR:37
for A being non empty Ordinal holds not Rank A is empty
proof end;

registration
let A be non empty Ordinal;
cluster Rank A -> non empty ;
coherence
not Rank A is empty by Th37;
end;

theorem :: CARD_LAR:38
for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Universe
proof end;