:: CARD_FIL semantic presentation

definition

let c₁, c₂ be set ;
redefine func \ as c₁ \ c₂ -> Subset of a₁;
coherence by XBOOLE_1:36;

end;

theorem Th1: :: CARD_FIL:1

for b₁ being set
for b₂ being infinite set holds Card {b₁} <` Card b₂

proof end;

registration

let c₁ be infinite set ;
cluster Card a₁ -> infinite ;
coherence by CARD_4:1;

end;

scheme :: CARD_FIL:sch 1
s1{ F₁() -> non empty set , F₂() -> set , P₁[ set ] } :

P₁[F₂()]

provided

E2: F₂() in { b₁ where B is Element of F₁() : P₁[b₁] }

proof end;

theorem Th2: :: CARD_FIL:2

for b₁ being non empty set holds
( {b₁} is non empty Subset-Family of b₁ & not {} in {b₁} & ( for b₂, b₃ being Subset of b₁ holds
( ( b₂ in {b₁} & b₃ in {b₁} implies b₂ /\ b₃ in {b₁} ) & ( b₂ in {b₁} & b₂ c= b₃ implies b₃ in {b₁} ) ) ) )

proof end;

definition

let c₁ be non empty set ;
mode Filter of c₁ -> non empty Subset-Family of a₁ means :Def1: :: CARD_FIL:def 1
( not {} in a₂ & ( for b₁, b₂ being Subset of a₁ holds
( ( b₁ in a₂ & b₂ in a₂ implies b₁ /\ b₂ in a₂ ) & ( b₁ in a₂ & b₁ c= b₂ implies b₂ in a₂ ) ) ) );
existence

proof end;

end;

:: deftheorem Def1 defines Filter CARD_FIL:def 1 :

theorem Th3: :: CARD_FIL:3

for b₁ being non empty set
for b₂ being set holds
( b₂ is Filter of b₁ iff ( b₂ is non empty Subset-Family of b₁ & not {} in b₂ & ( for b₃, b₄ being Subset of b₁ holds
( ( b₃ in b₂ & b₄ in b₂ implies b₃ /\ b₄ in b₂ ) & ( b₃ in b₂ & b₃ c= b₄ implies b₄ in b₂ ) ) ) ) ) by Def1;

theorem Th4: :: CARD_FIL:4

for b₁ being non empty set holds {b₁} is Filter of b₁

proof end;

theorem Th5: :: CARD_FIL:5

for b₁ being non empty set
for b₂ being Filter of b₁ holds b₁ in b₂

proof end;

theorem Th6: :: CARD_FIL:6

for b₁ being non empty set
for b₂ being Subset of b₁
for b₃ being Filter of b₁ st b₂ in b₃ holds
not b₁ \ b₂ in b₃

proof end;

theorem Th7: :: CARD_FIL:7

for b₁ being non empty set
for b₂ being Filter of b₁
for b₃ being non empty Subset-Family of b₁ st ( for b₄ being Subset of b₁ holds
( b₄ in b₃ iff b₄ ` in b₂ ) ) holds
( not b₁ in b₃ & ( for b₄, b₅ being Subset of b₁ holds
( ( b₄ in b₃ & b₅ in b₃ implies b₄ \/ b₅ in b₃ ) & ( b₄ in b₃ & b₅ c= b₄ implies b₅ in b₃ ) ) ) )

proof end;

notation

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
synonym dual c₂ for COMPLEMENT c₂;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty Subset-Family of c₁;
cluster dual a₂ -> non empty ;
coherence by SETFAM_1:46;

end;

theorem Th8: :: CARD_FIL:8

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ holds dual b₂ = { b₃ where B is Subset of b₁ : b₃ ` in b₂ }

proof end;

theorem Th9: :: CARD_FIL:9

for b₁ being non empty set
for b₂ being non empty Subset-Family of b₁ holds dual b₂ = { (b₃ ` ) where B is Subset of b₁ : b₃ in b₂ }

proof end;

definition

let c₁ be non empty set ;
mode Ideal of c₁ -> non empty Subset-Family of a₁ means :Def2: :: CARD_FIL:def 2
( not a₁ in a₂ & ( for b₁, b₂ being Subset of a₁ holds
( ( b₁ in a₂ & b₂ in a₂ implies b₁ \/ b₂ in a₂ ) & ( b₁ in a₂ & b₂ c= b₁ implies b₂ in a₂ ) ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines Ideal CARD_FIL:def 2 :

definition

let c₁ be non empty set ;
let c₂ be Filter of c₁;
redefine func dual as dual c₂ -> Ideal of a₁;
coherence

proof end;

end;

theorem Th10: :: CARD_FIL:10

for b₁ being non empty set
for b₂ being Filter of b₁
for b₃ being Ideal of b₁ holds
( ( for b₄ being Subset of b₁ holds
( not b₄ in b₂ or not b₄ in dual b₂ ) ) & ( for b₄ being Subset of b₁ holds
( not b₄ in b₃ or not b₄ in dual b₃ ) ) )

proof end;

theorem Th11: :: CARD_FIL:11

for b₁ being non empty set
for b₂ being Ideal of b₁ holds {} in b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Cardinal;
let c₃ be non empty Subset-Family of c₁;
pred c₃ is_multiplicative_with c₂ means :Def3: :: CARD_FIL:def 3
for b₁ being non empty set st b₁ c= a₃ & Card b₁ <` a₂ holds
meet b₁ in a₃;

end;

:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def 3 :

definition

let c₁ be non empty set ;
let c₂ be Cardinal;
let c₃ be non empty Subset-Family of c₁;
pred c₃ is_additive_with c₂ means :Def4: :: CARD_FIL:def 4
for b₁ being non empty set st b₁ c= a₃ & Card b₁ <` a₂ holds
union b₁ in a₃;

end;

:: deftheorem Def4 defines is_additive_with CARD_FIL:def 4 :

notation

let c₁ be non empty set ;
let c₂ be Cardinal;
let c₃ be Filter of c₁;
synonym c₃ is_complete_with c₂ for c₃ is_multiplicative_with c₂;

end;

notation

let c₁ be non empty set ;
let c₂ be Cardinal;
let c₃ be Ideal of c₁;
synonym c₃ is_complete_with c₂ for c₃ is_additive_with c₂;

end;

theorem Th12: :: CARD_FIL:12

for b₁ being Cardinal
for b₂ being non empty set
for b₃ being non empty Subset-Family of b₂ st b₃ is_multiplicative_with b₁ holds
dual b₃ is_additive_with b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be Filter of c₁;
attr a₂ is uniform means :Def5: :: CARD_FIL:def 5
for b₁ being Subset of a₁ st b₁ in a₂ holds
Card b₁ = Card a₁;
attr a₂ is principal means :Def6: :: CARD_FIL:def 6
ex b₁ being Subset of a₁ st
( b₁ in a₂ & ( for b₂ being Subset of a₁ st b₂ in a₂ holds
b₁ c= b₂ ) );
attr a₂ is being_ultrafilter means :Def7: :: CARD_FIL:def 7
for b₁ being Subset of a₁ holds
( b₁ in a₂ or a₁ \ b₁ in a₂ );

end;

:: deftheorem Def5 defines uniform CARD_FIL:def 5 :

:: deftheorem Def6 defines principal CARD_FIL:def 6 :

:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def 7 :

definition

let c₁ be non empty set ;
let c₂ be Filter of c₁;
let c₃ be Subset of c₁;
func Extend_Filter c₂,c₃ -> non empty Subset-Family of a₁ equals :: CARD_FIL:def 8
{ b₁ where B is Subset of a₁ : ex b₁ being Subset of a₁ st
( b₂ in { (b₃ /\ a₃) where B is Subset of a₁ : b₃ in a₂ } & b₂ c= b₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def8 defines Extend_Filter CARD_FIL:def 8 :

theorem Th13: :: CARD_FIL:13

for b₁ being non empty set
for b₂ being Subset of b₁
for b₃ being Filter of b₁
for b₄ being Subset of b₁ holds
( b₄ in Extend_Filter b₃,b₂ iff ex b₅ being Subset of b₁ st
( b₅ in b₃ & b₅ /\ b₂ c= b₄ ) )

proof end;

theorem Th14: :: CARD_FIL:14

for b₁ being non empty set
for b₂ being Subset of b₁
for b₃ being Filter of b₁ st ( for b₄ being Subset of b₁ st b₄ in b₃ holds
b₄ meets b₂ ) holds
( b₂ in Extend_Filter b₃,b₂ & Extend_Filter b₃,b₂ is Filter of b₁ & b₃ c= Extend_Filter b₃,b₂ )

proof end;

definition

let c₁ be non empty set ;
func Filters c₁ -> non empty Subset-Family of (bool a₁) equals :: CARD_FIL:def 9
{ b₁ where B is Subset-Family of a₁ : b₁ is Filter of a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Filters CARD_FIL:def 9 :

theorem Th15: :: CARD_FIL:15

for b₁ being non empty set
for b₂ being set holds
( b₂ in Filters b₁ iff b₂ is Filter of b₁ )

proof end;

theorem Th16: :: CARD_FIL:16

for b₁ being non empty set
for b₂ being non empty Subset of (Filters b₁) st b₂ is c=-linear holds
union b₂ is Filter of b₁

proof end;

theorem Th17: :: CARD_FIL:17

for b₁ being non empty set
for b₂ being Filter of b₁ ex b₃ being Filter of b₁ st
( b₂ c= b₃ & b₃ is being_ultrafilter )

proof end;

definition

let c₁ be infinite set ;
func Frechet_Filter c₁ -> Filter of a₁ equals :: CARD_FIL:def 10
{ b₁ where B is Subset of a₁ : Card (a₁ \ b₁) <` Card a₁ } ;
coherence

proof end;

end;

:: deftheorem Def10 defines Frechet_Filter CARD_FIL:def 10 :

definition

let c₁ be infinite set ;
func Frechet_Ideal c₁ -> Ideal of a₁ equals :: CARD_FIL:def 11
dual (Frechet_Filter a₁);
coherence ;

end;

:: deftheorem Def11 defines Frechet_Ideal CARD_FIL:def 11 :

theorem Th18: :: CARD_FIL:18

for b₁ being infinite set
for b₂ being Subset of b₁ holds
( b₂ in Frechet_Filter b₁ iff Card (b₁ \ b₂) <` Card b₁ )

proof end;

theorem Th19: :: CARD_FIL:19

for b₁ being infinite set
for b₂ being Subset of b₁ holds
( b₂ in Frechet_Ideal b₁ iff Card b₂ <` Card b₁ )

proof end;

theorem Th20: :: CARD_FIL:20

for b₁ being infinite set
for b₂ being Filter of b₁ st Frechet_Filter b₁ c= b₂ holds
b₂ is uniform

proof end;

theorem Th21: :: CARD_FIL:21

for b₁ being infinite set
for b₂ being Filter of b₁ st b₂ is uniform & b₂ is being_ultrafilter holds
Frechet_Filter b₁ c= b₂

proof end;

registration

let c₁ be infinite set ;
cluster non empty non principal being_ultrafilter Filter of a₁;
existence

proof end;

end;

registration

let c₁ be infinite set ;
cluster uniform being_ultrafilter -> non principal Filter of a₁;
coherence

proof end;

end;

theorem Th22: :: CARD_FIL:22

for b₁ being infinite set
for b₂ being being_ultrafilter Filter of b₁
for b₃ being Subset of b₁ holds
( b₃ in b₂ iff not b₃ in dual b₂ )

proof end;

theorem Th23: :: CARD_FIL:23

for b₁ being infinite set
for b₂ being Filter of b₁ st not b₂ is principal & b₂ is being_ultrafilter & b₂ is_complete_with Card b₁ holds
b₂ is uniform

proof end;

theorem Th24: :: CARD_FIL:24

for b₁ being Cardinal holds nextcard b₁ <=` exp 2,b₁

proof end;

definition

pred GCH means :Def12: :: CARD_FIL:def 12
for b₁ being Aleph holds nextcard b₁ = exp 2,b₁;

end;

:: deftheorem Def12 defines GCH CARD_FIL:def 12 :

definition

let c₁ be Aleph;
attr a₁ is inaccessible means :Def13: :: CARD_FIL:def 13
( a₁ is regular & a₁ is limit );

end;

:: deftheorem Def13 defines inaccessible CARD_FIL:def 13 :

notation

let c₁ be Aleph;
synonym c₁ is_inaccessible_cardinal for inaccessible c₁;

end;

registration

cluster inaccessible -> limit regular set ;
coherence by Def13;

end;

theorem Th25: :: CARD_FIL:25

alef 0 is inaccessible

proof end;

definition

let c₁ be Aleph;
attr a₁ is strong_limit means :Def14: :: CARD_FIL:def 14
for b₁ being Cardinal st b₁ <` a₁ holds
exp 2,b₁ <` a₁;

end;

:: deftheorem Def14 defines strong_limit CARD_FIL:def 14 :

notation

let c₁ be Aleph;
synonym c₁ is_strong_limit_cardinal for strong_limit c₁;

end;

theorem Th26: :: CARD_FIL:26

alef 0 is strong_limit

proof end;

theorem Th27: :: CARD_FIL:27

for b₁ being Aleph st b₁ is strong_limit holds
b₁ is limit

proof end;

registration

cluster strong_limit -> limit set ;
coherence by Th27;

end;

theorem Th28: :: CARD_FIL:28

for b₁ being Aleph st GCH & b₁ is limit holds
b₁ is strong_limit

proof end;

definition

let c₁ be Aleph;
attr a₁ is strongly_inaccessible means :Def15: :: CARD_FIL:def 15
( a₁ is regular & a₁ is strong_limit );

end;

:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def 15 :

notation

let c₁ be Aleph;
synonym c₁ is_strongly_inaccessible_cardinal for strongly_inaccessible c₁;

end;

registration

cluster strongly_inaccessible -> limit regular strong_limit set ;
coherence by Def15;

end;

theorem Th29: :: CARD_FIL:29

alef 0 is strongly_inaccessible by Def15, Th26, CARD_5:42;

theorem Th30: :: CARD_FIL:30

for b₁ being Aleph st b₁ is strongly_inaccessible holds
b₁ is inaccessible

proof end;

registration

cluster strongly_inaccessible -> limit regular inaccessible set ;
coherence by Th30;

end;

theorem Th31: :: CARD_FIL:31

for b₁ being Aleph st GCH & b₁ is inaccessible holds
b₁ is strongly_inaccessible

proof end;

definition

let c₁ be Aleph;
attr a₁ is measurable means :Def16: :: CARD_FIL:def 16
ex b₁ being Filter of a₁ st
( b₁ is_complete_with a₁ & not b₁ is principal & b₁ is being_ultrafilter );

end;

:: deftheorem Def16 defines measurable CARD_FIL:def 16 :

notation

let c₁ be Aleph;
synonym c₁ is_measurable_cardinal for measurable c₁;

end;

theorem Th32: :: CARD_FIL:32

for b₁ being being_limit_ordinal Ordinal
for b₂ being set st b₂ c= b₁ & sup b₂ = b₁ holds
union b₂ = b₁

proof end;

theorem Th33: :: CARD_FIL:33

for b₁ being Aleph st b₁ is measurable holds
b₁ is regular

proof end;

registration

let c₁ be Aleph;
cluster nextcard a₁ -> non limit ;
coherence

proof end;

end;

registration

cluster infinite non limit set ;
existence

proof end;

end;

registration

cluster non limit -> regular set ;
coherence

proof end;

end;

definition

let c₁ be non limit Cardinal;
func predecessor c₁ -> Cardinal means :Def17: :: CARD_FIL:def 17
a₁ = nextcard a₂;
existence by CARD_1:def 7;
uniqueness by CARD_4:21;

end;

:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :

registration

let c₁ be non limit Aleph;
cluster predecessor a₁ -> infinite ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be Cardinal;
mode Inf_Matrix of a₂,a₃,a₁ is Function of [:a₂,a₃:],a₁;

end;

definition

let c₁ be non limit Aleph;
let c₂ be Inf_Matrix of (predecessor c₁),c₁, bool c₁;
pred c₂ is_Ulam_Matrix_of c₁ means :Def18: :: CARD_FIL:def 18
( ( for b₁ being Element of predecessor a₁
for b₂, b₃ being Element of a₁ st b₂ <> b₃ holds
(a₂ . b₁,b₂) /\ (a₂ . b₁,b₃) is empty ) & ( for b₁ being Element of a₁
for b₂, b₃ being Element of predecessor a₁ st b₂ <> b₃ holds
(a₂ . b₂,b₁) /\ (a₂ . b₃,b₁) is empty ) & ( for b₁ being Element of predecessor a₁ holds Card (a₁ \ (union { (a₂ . b₁,b₂) where B is Element of a₁ : b₂ in a₁ } )) <=` predecessor a₁ ) & ( for b₁ being Element of a₁ holds Card (a₁ \ (union { (a₂ . b₂,b₁) where B is Element of predecessor a₁ : b₂ in predecessor a₁ } )) <=` predecessor a₁ ) );

end;

:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def 18 :

theorem Th34: :: CARD_FIL:34

for b₁ being non limit Aleph ex b₂ being Inf_Matrix of (predecessor b₁),b₁, bool b₁ st b₂ is_Ulam_Matrix_of b₁

proof end;

theorem Th35: :: CARD_FIL:35

for b₁ being non limit Aleph
for b₂ being Ideal of b₁ st b₂ is_complete_with b₁ & Frechet_Ideal b₁ c= b₂ holds
ex b₃ being Subset-Family of b₁ st
( Card b₃ = b₁ & ( for b₄ being set st b₄ in b₃ holds
not b₄ in b₂ ) & ( for b₄, b₅ being set st b₄ in b₃ & b₅ in b₃ & b₄ <> b₅ holds
b₄ misses b₅ ) )

proof end;

theorem Th36: :: CARD_FIL:36

for b₁ being set
for b₂ being Cardinal st b₂ <=` Card b₁ holds
ex b₃ being set st
( b₃ c= b₁ & Card b₃ = b₂ )

proof end;

theorem Th37: :: CARD_FIL:37

for b₁ being non limit Aleph
for b₂ being Filter of b₁ holds
( not b₂ is uniform or not b₂ is being_ultrafilter or not b₂ is_complete_with b₁ )

proof end;

theorem Th38: :: CARD_FIL:38

for b₁ being Aleph st b₁ is measurable holds
b₁ is limit

proof end;

theorem Th39: :: CARD_FIL:39

for b₁ being Aleph st b₁ is measurable holds
b₁ is inaccessible

proof end;

theorem Th40: :: CARD_FIL:40

for b₁ being Aleph st b₁ is measurable holds
b₁ is strong_limit

proof end;

theorem Th41: :: CARD_FIL:41

for b₁ being Aleph st b₁ is measurable holds
b₁ is strongly_inaccessible

proof end;