:: Basic facts about inaccessible and measurable cardinals
:: by Josef Urban
::
:: Received April 14, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

theorem :: CARD_FIL:1

for x being set
for X being infinite set holds card {x} in card X by CARD_3:103;

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

P₁[F₂()]

provided

A1: F₂() in { y where y is Element of F₁() : P₁[y] }

proof end;

theorem Th2: :: CARD_FIL:2

for X being non empty set holds
( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )

proof end;

definition

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

proof end;

end;

:: deftheorem Def1 defines Filter CARD_FIL:def 1 :
for X being non empty set
for b₂ being non empty Subset-Family of X holds
( b₂ is Filter of X iff ( not {} in b₂ & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b₂ & Y2 in b₂ implies Y1 /\ Y2 in b₂ ) & ( Y1 in b₂ & Y1 c= Y2 implies Y2 in b₂ ) ) ) ) );

theorem :: CARD_FIL:3

for X being non empty set
for F being set holds
( F is Filter of X iff ( F is non empty Subset-Family of X & not {} in F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) ) ) by Def1;

theorem Th4: :: CARD_FIL:4

for X being non empty set holds {X} is Filter of X

proof end;

theorem Th5: :: CARD_FIL:5

for X being non empty set
for F being Filter of X holds X in F

proof end;

theorem Th6: :: CARD_FIL:6

for X being non empty set
for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F

proof end;

theorem Th7: :: CARD_FIL:7

for X being non empty set
for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )

proof end;

notation

let X be non empty set ;
let S be Subset-Family of X;
synonym dual S for COMPLEMENT S;

end;

registration

let X be non empty set ;
let S be non empty Subset-Family of X;
cluster dual S -> non empty ;
coherence
not COMPLEMENT S is empty by SETFAM_1:46;

end;

theorem :: CARD_FIL:8

for X being non empty set
for S being non empty Subset-Family of X holds dual S = { Y where Y is Subset of X : Y ` in S }

proof end;

theorem Th9: :: CARD_FIL:9

for X being non empty set
for S being non empty Subset-Family of X holds dual S = { (Y `) where Y is Subset of X : Y in S }

proof end;

definition

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

proof end;

end;

:: deftheorem Def2 defines Ideal CARD_FIL:def 2 :
for X being non empty set
for b₂ being non empty Subset-Family of X holds
( b₂ is Ideal of X iff ( not X in b₂ & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b₂ & Y2 in b₂ implies Y1 \/ Y2 in b₂ ) & ( Y1 in b₂ & Y2 c= Y1 implies Y2 in b₂ ) ) ) ) );

definition

let X be non empty set ;
let F be Filter of X;
:: original: dual
redefine func dual F -> Ideal of X;
coherence
dual F is Ideal of X

proof end;

end;

theorem Th10: :: CARD_FIL:10

for X being non empty set
for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )

proof end;

theorem Th11: :: CARD_FIL:11

for X being non empty set
for I being Ideal of X holds {} in I

proof end;

definition

let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
pred S is_multiplicative_with N means :Def3: :: CARD_FIL:def 3
for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S;

end;

:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def 3 :
for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_multiplicative_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S );

definition

let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
pred S is_additive_with N means :Def4: :: CARD_FIL:def 4
for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S;

end;

:: deftheorem Def4 defines is_additive_with CARD_FIL:def 4 :
for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_additive_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S );

notation

let X be non empty set ;
let N be Cardinal;
let F be Filter of X;
synonym F is_complete_with N for F is_multiplicative_with N;

end;

notation

let X be non empty set ;
let N be Cardinal;
let I be Ideal of X;
synonym I is_complete_with N for I is_additive_with N;

end;

theorem Th12: :: CARD_FIL:12

for N being Cardinal
for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N

proof end;

definition

let X be non empty set ;
let F be Filter of X;
attr F is uniform means :Def5: :: CARD_FIL:def 5
for Y being Subset of X st Y in F holds
card Y = card X;
attr F is principal means :Def6: :: CARD_FIL:def 6
ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) );
attr F is being_ultrafilter means :Def7: :: CARD_FIL:def 7
for Y being Subset of X holds
( Y in F or X \ Y in F );

end;

:: deftheorem Def5 defines uniform CARD_FIL:def 5 :
for X being non empty set
for F being Filter of X holds
( F is uniform iff for Y being Subset of X st Y in F holds
card Y = card X );

:: deftheorem Def6 defines principal CARD_FIL:def 6 :
for X being non empty set
for F being Filter of X holds
( F is principal iff ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) ) );

:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def 7 :
for X being non empty set
for F being Filter of X holds
( F is being_ultrafilter iff for Y being Subset of X holds
( Y in F or X \ Y in F ) );

definition

let X be non empty set ;
let F be Filter of X;
let Z be Subset of X;
func Extend_Filter (F,Z) -> non empty Subset-Family of X equals :: CARD_FIL:def 8
{ Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;
coherence
{ Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } is non empty Subset-Family of X

proof end;

end;

:: deftheorem defines Extend_Filter CARD_FIL:def 8 :
for X being non empty set
for F being Filter of X
for Z being Subset of X holds Extend_Filter (F,Z) = { Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;

theorem Th13: :: CARD_FIL:13

for X being non empty set
for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )

proof end;

theorem Th14: :: CARD_FIL:14

for X being non empty set
for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )

proof end;

definition

let X be non empty set ;
func Filters X -> non empty Subset-Family of (bool X) equals :: CARD_FIL:def 9
{ S where S is Subset-Family of X : S is Filter of X } ;
coherence
{ S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X)

proof end;

end;

:: deftheorem defines Filters CARD_FIL:def 9 :
for X being non empty set holds Filters X = { S where S is Subset-Family of X : S is Filter of X } ;

theorem Th15: :: CARD_FIL:15

for X being non empty set
for S being set holds
( S in Filters X iff S is Filter of X )

proof end;

theorem Th16: :: CARD_FIL:16

for X being non empty set
for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X

proof end;

theorem Th17: :: CARD_FIL:17

for X being non empty set
for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )

proof end;

definition

let X be infinite set ;
func Frechet_Filter X -> Filter of X equals :: CARD_FIL:def 10
{ Y where Y is Subset of X : card (X \ Y) in card X } ;
coherence
{ Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X

proof end;

end;

:: deftheorem defines Frechet_Filter CARD_FIL:def 10 :
for X being infinite set holds Frechet_Filter X = { Y where Y is Subset of X : card (X \ Y) in card X } ;

definition

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

end;

:: deftheorem defines Frechet_Ideal CARD_FIL:def 11 :
for X being infinite set holds Frechet_Ideal X = dual (Frechet_Filter X);

theorem Th18: :: CARD_FIL:18

for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )

proof end;

theorem Th19: :: CARD_FIL:19

for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )

proof end;

theorem Th20: :: CARD_FIL:20

for X being infinite set
for F being Filter of X st Frechet_Filter X c= F holds
F is uniform

proof end;

theorem :: CARD_FIL:21

for X being infinite set
for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf

proof end;

registration

let X be infinite set ;
cluster non empty non principal being_ultrafilter Filter of X;
existence
ex b₁ being Filter of X st
( not b₁ is principal & b₁ is being_ultrafilter )

proof end;

end;

registration

let X be infinite set ;
cluster uniform being_ultrafilter -> non principal Filter of X;
coherence
for b₁ being Filter of X st b₁ is uniform & b₁ is being_ultrafilter holds
not b₁ is principal

proof end;

end;

theorem Th22: :: CARD_FIL:22

for X being infinite set
for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )

proof end;

theorem Th23: :: CARD_FIL:23

for X being infinite set
for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform

proof end;

begin

theorem Th24: :: CARD_FIL:24

for N being Cardinal holds nextcard N c= exp (2,N)

proof end;

definition

pred GCH means :Def12: :: CARD_FIL:def 12
for N being Aleph holds nextcard N = exp (2,N);

end;

:: deftheorem Def12 defines GCH CARD_FIL:def 12 :
( GCH iff for N being Aleph holds nextcard N = exp (2,N) );

definition

let IT be Aleph;
attr IT is inaccessible means :Def13: :: CARD_FIL:def 13
( IT is regular & IT is limit_cardinal );

end;

:: deftheorem Def13 defines inaccessible CARD_FIL:def 13 :
for IT being Aleph holds
( IT is inaccessible iff ( IT is regular & IT is limit_cardinal ) );

registration

cluster non finite cardinal inaccessible -> limit_cardinal regular set ;
coherence
for b₁ being Aleph st b₁ is inaccessible holds
( b₁ is regular & b₁ is limit_cardinal ) by Def13;

end;

theorem :: CARD_FIL:25

omega is inaccessible

proof end;

definition

let IT be Aleph;
attr IT is strong_limit means :Def14: :: CARD_FIL:def 14
for N being Cardinal st N in IT holds
exp (2,N) in IT;

end;

:: deftheorem Def14 defines strong_limit CARD_FIL:def 14 :
for IT being Aleph holds
( IT is strong_limit iff for N being Cardinal st N in IT holds
exp (2,N) in IT );

theorem Th26: :: CARD_FIL:26

omega is strong_limit

proof end;

theorem Th27: :: CARD_FIL:27

for M being Aleph st M is strong_limit holds
M is limit_cardinal

proof end;

registration

cluster non finite cardinal strong_limit -> limit_cardinal set ;
coherence
for b₁ being Aleph st b₁ is strong_limit holds
b₁ is limit_cardinal by Th27;

end;

theorem Th28: :: CARD_FIL:28

for M being Aleph st GCH & M is limit_cardinal holds
M is strong_limit

proof end;

definition

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

end;

:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def 15 :
for IT being Aleph holds
( IT is strongly_inaccessible iff ( IT is regular & IT is strong_limit ) );

registration

cluster non finite cardinal strongly_inaccessible -> regular strong_limit set ;
coherence
for b₁ being Aleph st b₁ is strongly_inaccessible holds
( b₁ is regular & b₁ is strong_limit ) by Def15;

end;

theorem :: CARD_FIL:29

omega is strongly_inaccessible by Def15, Th26, CARD_5:42;

theorem Th30: :: CARD_FIL:30

for M being Aleph st M is strongly_inaccessible holds
M is inaccessible

proof end;

registration

cluster non finite cardinal strongly_inaccessible -> inaccessible set ;
coherence
for b₁ being Aleph st b₁ is strongly_inaccessible holds
b₁ is inaccessible by Th30;

end;

theorem :: CARD_FIL:31

for M being Aleph st GCH & M is inaccessible holds
M is strongly_inaccessible

proof end;

definition

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

end;

:: deftheorem Def16 defines measurable CARD_FIL:def 16 :
for M being Aleph holds
( M is measurable iff ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter ) );

theorem Th32: :: CARD_FIL:32

for A being limit_ordinal Ordinal
for X being set st X c= A & sup X = A holds
union X = A

proof end;

theorem Th33: :: CARD_FIL:33

for M being Aleph st M is measurable holds
M is regular

proof end;

registration

let M be Aleph;
cluster nextcard M -> non limit_cardinal ;
coherence
not nextcard M is limit_cardinal

proof end;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal infinite cardinal non limit_cardinal set ;
existence
ex b₁ being Cardinal st
( not b₁ is limit_cardinal & not b₁ is finite )

proof end;

end;

registration

cluster non finite cardinal non limit_cardinal -> regular set ;
coherence
for b₁ being Aleph st not b₁ is limit_cardinal holds
b₁ is regular

proof end;

end;

definition

let M be non limit_cardinal Cardinal;
func predecessor M -> Cardinal means :Def17: :: CARD_FIL:def 17
M = nextcard it;
existence
ex b₁ being Cardinal st M = nextcard b₁ by CARD_1:def 7;
uniqueness
for b₁, b₂ being Cardinal st M = nextcard b₁ & M = nextcard b₂ holds
b₁ = b₂ by CARD_3:106;

end;

:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :
for M being non limit_cardinal Cardinal
for b₂ being Cardinal holds
( b₂ = predecessor M iff M = nextcard b₂ );

registration

let M be non limit_cardinal Aleph;
cluster predecessor M -> infinite ;
coherence
not predecessor M is finite

proof end;

end;

definition

let X be set ;
let N, N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;

end;

definition

let M be non limit_cardinal Aleph;
let T be Inf_Matrix of (predecessor M),M,(bool M);
pred T is_Ulam_Matrix_of M means :Def18: :: CARD_FIL:def 18
( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) );

end;

:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def 18 :
for M being non limit_cardinal Aleph
for T being Inf_Matrix of (predecessor M),M,(bool M) holds
( T is_Ulam_Matrix_of M iff ( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) ) );

theorem Th34: :: CARD_FIL:34

for M being non limit_cardinal Aleph ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M

proof end;

theorem Th35: :: CARD_FIL:35

for M being non limit_cardinal Aleph
for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )

proof end;

theorem Th36: :: CARD_FIL:36

for X being set
for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )

proof end;

theorem Th37: :: CARD_FIL:37

for M being non limit_cardinal Aleph
for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )

proof end;

theorem Th38: :: CARD_FIL:38

for M being Aleph st M is measurable holds
M is limit_cardinal

proof end;

theorem :: CARD_FIL:39

for M being Aleph st M is measurable holds
M is inaccessible

proof end;

theorem Th40: :: CARD_FIL:40

for M being Aleph st M is measurable holds
M is strong_limit

proof end;

theorem :: CARD_FIL:41

for M being Aleph st M is measurable holds
M is strongly_inaccessible

proof end;