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


begin

:: ::
:: 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
proofend;
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
proofend;
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 )
proofend;
end;

definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
predX is_unbounded_in A means :Def1: :: CARD_LAR:def 1
( X c= A & sup X = A );
predX is_closed_in A means :Def2: :: 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 Def1 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 Def2 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 ;
predX is_club_in A means :Def3: :: CARD_LAR:def 3
( X is_closed_in A & X is_unbounded_in A );
end;

:: deftheorem Def3 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;
attrX is unbounded  means :Def4: :: CARD_LAR:def 4
 sup X = A;
attrX is closed  means :Def5: :: 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 Def4 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 Def5 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 ) )
proofend;

:: 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
proofend;

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
proofend;

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 ) )
proofend;

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 )
proofend;

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 ) )
proofend;

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
proofend;

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 )  }
proofend;

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
proofend;
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) )
proofend;

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

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 )
proofend;

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 )
proofend;

definition
let A be limit_ordinal infinite Ordinal;
let X be Subset of A;
attrX is stationary  means :Def7: :: 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 Def7 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
proofend;

definition
let A be limit_ordinal infinite Ordinal;
let X be set ;
predX is_stationary_in A means :Def8: :: 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 Def8 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 :: 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
proofend;

:: 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
proofend;
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
proofend;

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
proofend;
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 B3, B1 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
proofend;

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
proofend;

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

:: 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 )
proofend;

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 )
proofend;
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
proofend;

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
proofend;

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 Function of NAT,X holds sup (rng f) in M
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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

:: deftheorem Def10 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 Def11 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
proofend;

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

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

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

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

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

begin

:: 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
proofend;

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
proofend;

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
proofend;

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

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

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

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
proofend;