:: CARD_LAR semantic presentation

definition

let c₁, c₂ be set ;
let c₃ be Subset of c₁;
redefine func /\ as c₂ /\ c₃ -> Subset of a₁;
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 c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be set ;
pred c₂ is_unbounded_in c₁ means :Def1: :: CARD_LAR:def 1
( a₂ c= a₁ & sup a₂ = a₁ );
pred c₂ is_closed_in c₁ means :Def2: :: CARD_LAR:def 2
( a₂ c= a₁ & ( for b₁ being being_limit_ordinal infinite Ordinal st b₁ in a₁ & sup (a₂ /\ b₁) = b₁ holds
b₁ in a₂ ) );

end;

:: deftheorem Def1 defines is_unbounded_in CARD_LAR:def 1 :

:: deftheorem Def2 defines is_closed_in CARD_LAR:def 2 :

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be set ;
pred c₂ is_club_in c₁ means :Def3: :: CARD_LAR:def 3
( a₂ is_closed_in a₁ & a₂ is_unbounded_in a₁ );

end;

:: deftheorem Def3 defines is_club_in CARD_LAR:def 3 :

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be Subset of c₁;
attr a₂ is unbounded means :Def4: :: CARD_LAR:def 4
sup a₂ = a₁;
attr a₂ is closed means :Def5: :: CARD_LAR:def 5
for b₁ being being_limit_ordinal infinite Ordinal st b₁ in a₁ & sup (a₂ /\ b₁) = b₁ holds
b₁ in a₂;

end;

:: deftheorem Def4 defines unbounded CARD_LAR:def 4 :

:: deftheorem Def5 defines closed CARD_LAR:def 5 :

notation

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be Subset of c₁;
antonym bounded c₂ for unbounded c₂;

end;

theorem Th1: :: CARD_LAR:1

canceled;

theorem Th2: :: CARD_LAR:2

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ holds
( b₂ is_club_in b₁ iff ( b₂ is closed & b₂ is unbounded ) )

proof end;

theorem Th3: :: CARD_LAR:3

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ holds b₂ c= sup b₂

proof end;

theorem Th4: :: CARD_LAR:4

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ st not b₂ is empty & ( for b₃ being Ordinal st b₃ in b₂ holds
ex b₄ being Ordinal st
( b₄ in b₂ & b₃ in b₄ ) ) holds
sup b₂ is being_limit_ordinal infinite Ordinal

proof end;

theorem Th5: :: CARD_LAR:5

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ holds
( not b₂ is unbounded iff ex b₃ being Ordinal st
( b₃ in b₁ & b₂ c= b₃ ) )

proof end;

theorem Th6: :: CARD_LAR:6

for b₁, b₂ being being_limit_ordinal infinite Ordinal
for b₃ being Subset of b₁ st not sup (b₃ /\ b₂) = b₂ holds
ex b₄ being Ordinal st
( b₄ in b₂ & b₃ /\ b₂ c= b₄ )

proof end;

theorem Th7: :: CARD_LAR:7

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ holds
( b₂ is unbounded iff for b₃ being Ordinal st b₃ in b₁ holds
ex b₄ being Ordinal st
( b₄ in b₂ & b₃ c= b₄ ) )

proof end;

theorem Th8: :: CARD_LAR:8

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ st b₂ is unbounded holds
not b₂ is empty

proof end;

theorem Th9: :: CARD_LAR:9

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Ordinal
for b₃ being Subset of b₁ st b₃ is unbounded & b₂ in b₁ holds
ex b₄ being Element of b₁ st b₄ in { b₅ where B is Element of b₁ : ( b₅ in b₃ & b₂ in b₅ ) }

proof end;

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be Subset of c₁;
let c₃ be Ordinal;
assume E14: c₂ is unbounded ;
assume E15: c₃ in c₁ ;
func LBound c₃,c₂ -> Element of a₂ equals :Def6: :: CARD_LAR:def 6
inf { b₁ where B is Element of a₁ : ( b₁ in a₂ & a₃ in b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines LBound CARD_LAR:def 6 :

theorem Th10: :: CARD_LAR:10

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Ordinal
for b₃ being Subset of b₁ st b₃ is unbounded & b₂ in b₁ holds
( LBound b₂,b₃ in b₃ & b₂ in LBound b₂,b₃ )

proof end;

theorem Th11: :: CARD_LAR:11

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

proof end;

definition

let c₁ be set ;
let c₂ be Subset of c₁;
let c₃ be set ;
redefine func \ as c₂ \ c₃ -> Subset of a₁;
coherence

proof end;

end;

theorem Th12: :: CARD_LAR:12

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Ordinal
for b₃ being Subset of b₁ st b₂ in b₁ & b₃ is closed & b₃ is unbounded holds
( b₃ \ b₂ is closed & b₃ \ b₂ is unbounded )

proof end;

theorem Th13: :: CARD_LAR:13

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Ordinal st b₂ in b₁ holds
( b₁ \ b₂ is closed & b₁ \ b₂ is unbounded )

proof end;

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be Subset of c₁;
attr a₂ is stationary means :Def7: :: CARD_LAR:def 7
for b₁ being Subset of a₁ st b₁ is closed & b₁ is unbounded holds
not a₂ /\ b₁ is empty;

end;

:: deftheorem Def7 defines stationary CARD_LAR:def 7 :

theorem Th14: :: CARD_LAR:14

for b₁ being being_limit_ordinal infinite Ordinal
for b₂, b₃ being Subset of b₁ st b₂ is stationary & b₂ c= b₃ holds
b₃ is stationary

proof end;

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be set ;
pred c₂ is_stationary_in c₁ means :Def8: :: CARD_LAR:def 8
( a₂ c= a₁ & ( for b₁ being Subset of a₁ st b₁ is closed & b₁ is unbounded holds
not a₂ /\ b₁ is empty ) );

end;

:: deftheorem Def8 defines is_stationary_in CARD_LAR:def 8 :

theorem Th15: :: CARD_LAR:15

for b₁ being being_limit_ordinal infinite Ordinal
for b₂, b₃ being set st b₂ is_stationary_in b₁ & b₂ c= b₃ & b₃ c= b₁ holds
b₃ is_stationary_in b₁

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
redefine mode Element as Element of c₂ -> Subset of a₁;
coherence

proof end;

end;

theorem Th16: :: CARD_LAR:16

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ st b₂ is stationary holds
b₂ is unbounded

proof end;

definition

let c₁ be being_limit_ordinal infinite Ordinal;
let c₂ be Subset of c₁;
func limpoints c₂ -> Subset of a₁ equals :: CARD_LAR:def 9
{ b₁ where B is Element of a₁ : ( not b₁ is finite & b₁ is being_limit_ordinal & sup (a₂ /\ b₁) = b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines limpoints CARD_LAR:def 9 :

theorem Th17: :: CARD_LAR:17

for b₁ being being_limit_ordinal infinite Ordinal
for b₂, b₃ being Ordinal
for b₄ being Subset of b₁ st b₄ /\ b₂ c= b₃ holds
b₂ /\ (limpoints b₄) c= succ b₃

proof end;

theorem Th18: :: CARD_LAR:18

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Ordinal
for b₃ being Subset of b₁ st b₃ c= b₂ holds
limpoints b₃ c= succ b₂

proof end;

theorem Th19: :: CARD_LAR:19

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ holds limpoints b₂ is closed

proof end;

theorem Th20: :: CARD_LAR:20

for b₁ being being_limit_ordinal infinite Ordinal
for b₂ being Subset of b₁ st b₂ is unbounded & not limpoints b₂ is unbounded holds
ex b₃ being Ordinal st
( b₃ in b₁ & { (succ b₄) where B is Element of b₁ : ( b₄ in b₂ & b₃ in succ b₄ ) } is_club_in b₁ )

proof end;

registration

let c₁ be non countable Aleph;
cluster being_limit_ordinal infinite cardinal Element of a₁;
existence

proof end;

end;

theorem Th21: :: CARD_LAR:21

for b₁ being Aleph
for b₂ being Subset of b₁ st b₂ is unbounded holds
cf b₁ <=` Card b₂

proof end;

theorem Th22: :: CARD_LAR:22

for b₁ being non countable Aleph
for b₂ being Subset-Family of b₁ st ( for b₃ being Element of b₂ holds b₃ is closed ) holds
meet b₂ is closed

proof end;

theorem Th23: :: CARD_LAR:23

for b₁ being non countable Aleph
for b₂ being Subset of b₁ st alef 0 <` cf b₁ holds
for b₃ being Function of NAT ,b₂ holds sup (rng b₃) in b₁

proof end;

theorem Th24: :: CARD_LAR:24

for b₁ being non countable Aleph st alef 0 <` cf b₁ holds
for b₂ being non empty Subset-Family of b₁ st Card b₂ <` cf b₁ & ( for b₃ being Element of b₂ holds
( b₃ is closed & b₃ is unbounded ) ) holds
( meet b₂ is closed & meet b₂ is unbounded )

proof end;

theorem Th25: :: CARD_LAR:25

for b₁ being non countable Aleph
for b₂ being Subset of b₁ st alef 0 <` cf b₁ & b₂ is unbounded holds
for b₃ being Ordinal st b₃ in b₁ holds
ex b₄ being being_limit_ordinal infinite Ordinal st
( b₄ in b₁ & b₃ in b₄ & b₄ in limpoints b₂ )

proof end;

theorem Th26: :: CARD_LAR:26

for b₁ being non countable Aleph
for b₂ being Subset of b₁ st alef 0 <` cf b₁ & b₂ is unbounded holds
limpoints b₂ is unbounded

proof end;

definition

let c₁ be non countable Aleph;
attr a₁ is Mahlo means :Def10: :: CARD_LAR:def 10
{ b₁ where B is infinite cardinal Element of a₁ : b₁ is regular } is_stationary_in a₁;
attr a₁ is strongly_Mahlo means :Def11: :: CARD_LAR:def 11
{ b₁ where B is infinite cardinal Element of a₁ : b₁ is strongly_inaccessible } is_stationary_in a₁;

end;

:: deftheorem Def10 defines Mahlo CARD_LAR:def 10 :

:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def 11 :

notation

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

end;

theorem Th27: :: CARD_LAR:27

for b₁ being non countable Aleph st b₁ is strongly_Mahlo holds
b₁ is Mahlo

proof end;

theorem Th28: :: CARD_LAR:28

for b₁ being non countable Aleph st b₁ is Mahlo holds
b₁ is regular

proof end;

theorem Th29: :: CARD_LAR:29

for b₁ being non countable Aleph st b₁ is Mahlo holds
b₁ is limit

proof end;

theorem Th30: :: CARD_LAR:30

for b₁ being non countable Aleph st b₁ is Mahlo holds
b₁ is inaccessible

proof end;

theorem Th31: :: CARD_LAR:31

for b₁ being non countable Aleph st b₁ is strongly_Mahlo holds
b₁ is strong_limit

proof end;

theorem Th32: :: CARD_LAR:32

for b₁ being non countable Aleph st b₁ is strongly_Mahlo holds
b₁ is strongly_inaccessible

proof end;

theorem Th33: :: CARD_LAR:33

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
ex b₃ being set st
( b₃ in b₁ & b₂ c= b₃ & b₃ is Cardinal ) ) holds
union b₁ is Cardinal

proof end;

theorem Th34: :: CARD_LAR:34

for b₁ being set
for b₂ being Aleph st Card b₁ <` cf b₂ & ( for b₃ being set st b₃ in b₁ holds
Card b₃ <` b₂ ) holds
Card (union b₁) in b₂

proof end;

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

theorem Th35: :: CARD_LAR:35

for b₁ being non countable Aleph
for b₂ being Ordinal st b₁ is strongly_inaccessible & b₂ in b₁ holds
Card (Rank b₂) <` b₁

proof end;

theorem Th36: :: CARD_LAR:36

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

proof end;

theorem Th37: :: CARD_LAR:37

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

proof end;

theorem Th38: :: CARD_LAR:38

for b₁ being non empty Ordinal holds not Rank b₁ is empty

proof end;

registration

let c₁ be non empty Ordinal;
cluster Rank a₁ -> non empty ;
coherence by Th38;

end;

theorem Th39: :: CARD_LAR:39

for b₁ being non countable Aleph st b₁ is strongly_inaccessible holds
Rank b₁ is Universe

proof end;

theorem Th40: :: CARD_LAR:40

for b₁ being non countable Aleph st b₁ is strongly_inaccessible holds
Rank b₁ is being_a_model_of_ZF

proof end;