:: CARD_LAR semantic presentation

definition

let S, X be set ;
let Y be Subset of S;
:: original: /\
redefine func X /\ Y -> Subset of S;
coherence

proof end;

end;

registration

cluster infinite cardinal -> being_limit_ordinal set ;
coherence by CARD_4:32;

end;

registration

cluster non empty being_limit_ordinal -> infinite set ;
coherence

proof end;

end;

registration

cluster non limit -> being_limit_ordinal non countable set ;
coherence

proof end;

end;

registration

cluster being_limit_ordinal regular non countable set ;
existence

proof end;

end;

definition

let A be being_limit_ordinal infinite Ordinal;
let X be set ;
pred X is_unbounded_in A means :Def1: :: CARD_LAR:def 1
( X c= A & sup X = A );
pred X is_closed_in A means :Def2: :: CARD_LAR:def 2
( X c= A & ( for B being 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 :

:: deftheorem Def2 defines is_closed_in CARD_LAR:def 2 :

definition

let A be being_limit_ordinal infinite Ordinal;
let X be set ;
pred X 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 :

definition

let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X is unbounded means :Def4: :: CARD_LAR:def 4
sup X = A;
attr X is closed means :Def5: :: CARD_LAR:def 5
for B being 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 :

:: deftheorem Def5 defines closed CARD_LAR:def 5 :

notation

let A be being_limit_ordinal infinite Ordinal;
let X be Subset of A;
antonym bounded X for unbounded X;

end;

theorem :: CARD_LAR:1

canceled;

theorem Th2: :: CARD_LAR:2

for A being 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;

theorem Th3: :: CARD_LAR:3

for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds X c= sup X

proof end;

theorem Th4: :: CARD_LAR:4

for A being 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 being_limit_ordinal infinite Ordinal

proof end;

theorem Th5: :: CARD_LAR:5

for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds
( not X is unbounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )

proof end;

theorem Th6: :: CARD_LAR:6

for A, B being 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 Th7: :: CARD_LAR:7

for A being 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 Th8: :: CARD_LAR:8

for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded holds
not X is empty

proof end;

theorem Th9: :: CARD_LAR:9

for A being 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 being_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

proof end;

end;

:: deftheorem Def6 defines LBound CARD_LAR:def 6 :

theorem Th10: :: CARD_LAR:10

for A being 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 Th11: :: CARD_LAR:11

for A being being_limit_ordinal infinite Ordinal holds
( [#] A is closed & [#] A is unbounded )

proof end;

definition

let A be set ;
let X be Subset of A;
let Y be set ;
:: original: \
redefine func X \ Y -> Subset of A;
coherence

proof end;

end;

theorem Th12: :: CARD_LAR:12

for A being 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 Th13: :: CARD_LAR:13

for A being 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 being_limit_ordinal infinite Ordinal;
let X be Subset of A;
attr X 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 :

theorem Th14: :: CARD_LAR:14

for A being 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 being_limit_ordinal infinite Ordinal;
let X be set ;
pred X 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 :

theorem :: CARD_LAR:15

for A being 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;

definition

let X be set ;
let S be Subset-Family of X;
:: original: Element
redefine mode Element of S -> Subset of X;
coherence

proof end;

end;

theorem :: CARD_LAR:16

for A being 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 being_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 : ( not B1 is finite & B1 is being_limit_ordinal & sup (X /\ B1) = B1 ) } ;
coherence

proof end;

end;

:: deftheorem defines limpoints CARD_LAR:def 9 :

theorem Th17: :: CARD_LAR:17

for A being 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

proof end;

theorem :: CARD_LAR:18

for A being 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 Th19: :: CARD_LAR:19

for A being being_limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X is closed

proof end;

theorem Th20: :: CARD_LAR:20

for A being being_limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded & not limpoints X is unbounded 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 being_limit_ordinal infinite cardinal Element of M;
existence

proof end;

end;

theorem Th21: :: CARD_LAR:21

for M being Aleph
for X being Subset of M st X is unbounded holds
cf M <=` Card X

proof end;

theorem Th22: :: CARD_LAR:22

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 Th23: :: CARD_LAR:23

for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M holds
for f being Function of NAT ,X holds sup (rng f) in M

proof end;

theorem :: CARD_LAR:24

for M being non countable Aleph st alef 0 <` cf M holds
for S being non empty Subset-Family of M st Card S <` 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 Th25: :: CARD_LAR:25

for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M & X is unbounded holds
for B1 being Ordinal st B1 in M holds
ex B being being_limit_ordinal infinite Ordinal st
( B in M & B1 in B & B in limpoints X )

proof end;

theorem :: CARD_LAR:26

for M being non countable Aleph
for X being Subset of M st alef 0 <` cf M & X is unbounded holds
limpoints X is unbounded

proof end;

definition

let M be non countable Aleph;
attr M is Mahlo means :Def10: :: 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 :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 :

:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def 11 :

notation

let M be non countable Aleph;
synonym M is_Mahlo for Mahlo M;
synonym M is_strongly_Mahlo for strongly_Mahlo M;

end;

theorem Th27: :: CARD_LAR:27

for M being non countable Aleph st M is strongly_Mahlo holds
M is Mahlo

proof end;

theorem Th28: :: CARD_LAR:28

for M being non countable Aleph st M is Mahlo holds
M is regular

proof end;

theorem Th29: :: CARD_LAR:29

for M being non countable Aleph st M is Mahlo holds
M is limit

proof end;

theorem :: CARD_LAR:30

for M being non countable Aleph st M is Mahlo holds
M is inaccessible

proof end;

theorem Th31: :: CARD_LAR:31

for M being non countable Aleph st M is strongly_Mahlo holds
M is strong_limit

proof end;

theorem :: CARD_LAR:32

for M being non countable Aleph st M is strongly_Mahlo holds
M is strongly_inaccessible

proof end;

theorem Th33: :: CARD_LAR:33

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 Th34: :: CARD_LAR:34

for X being set
for M being Aleph st Card X <` cf M & ( for Y being set st Y in X holds
Card Y <` M ) holds
Card (union X) in M

proof end;

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

theorem Th35: :: CARD_LAR:35

for M being non countable Aleph
for A being Ordinal st M is strongly_inaccessible & A in M holds
Card (Rank A) <` M

proof end;

theorem Th36: :: CARD_LAR:36

for M being non countable Aleph st M is strongly_inaccessible holds
Card (Rank M) = M

proof end;

theorem Th37: :: CARD_LAR:37

for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_Tarski-Class

proof end;

theorem Th38: :: CARD_LAR:38

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 by Th38;

end;

theorem Th39: :: CARD_LAR:39

for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is Universe

proof end;

theorem :: CARD_LAR:40

for M being non countable Aleph st M is strongly_inaccessible holds
Rank M is being_a_model_of_ZF

proof end;