:: Basic facts about inaccessible and measurable cardinals
:: by Josef Urban
::
:: Copyright (c) 2000-2017 Association of Mizar Users

theorem :: CARD_FIL:1
for x being set
for X being infinite set holds card {x} in card X by CARD_3:86;

scheme :: CARD_FIL:sch 1
ElemProp{ F1() -> non empty set , F2() -> set , P1[ set ] } :
P1[F2()]
provided
A1: F2() in { y where y is Element of F1() : P1[y] }
proof end;

:: Necessary facts about filters and ideals on sets
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 b1 being non empty Subset-Family of X st
( not {} in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 /\ Y2 in b1 ) & ( Y1 in b1 & Y1 c= Y2 implies Y2 in b1 ) ) ) )
proof end;
end;

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

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:32;
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 b1 being non empty Subset-Family of X st
( not X in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 \/ Y2 in b1 ) & ( Y1 in b1 & Y2 c= Y1 implies Y2 in b1 ) ) ) )
proof end;
end;

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

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 :: 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 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 :: 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 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
proof end;

definition
let X be non empty set ;
let F be Filter of X;
attr F is uniform means :: CARD_FIL:def 5
for Y being Subset of X st Y in F holds
card Y = card X;
attr F is principal means :: 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 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 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 () 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 ();
coherence
dual () is Ideal of X
;
end;

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

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 for Filter of X;
existence
ex b1 being Filter of X st
( not b1 is principal & b1 is being_ultrafilter )
proof end;
end;

registration
let X be infinite set ;
cluster uniform being_ultrafilter -> non principal for Filter of X;
coherence
for b1 being Filter of X st b1 is uniform & b1 is being_ultrafilter holds
not b1 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;

theorem Th24: :: CARD_FIL:24
for N being Cardinal holds nextcard N c= exp (2,N)
proof end;

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

:: deftheorem 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 :: CARD_FIL:def 13
( IT is regular & IT is limit_cardinal );
end;

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

registration
coherence
for b1 being Aleph st b1 is inaccessible holds
( b1 is regular & b1 is limit_cardinal )
;
end;

theorem :: CARD_FIL:25

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

:: deftheorem 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
proof end;

theorem Th27: :: CARD_FIL:27
for M being Aleph st M is strong_limit holds
M is limit_cardinal
proof end;

registration
coherence
for b1 being Aleph st b1 is strong_limit holds
b1 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 :: CARD_FIL:def 15
( IT is regular & IT is strong_limit );
end;

:: deftheorem 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
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
( b1 is regular & b1 is strong_limit )
;
end;

theorem :: CARD_FIL:29

theorem :: CARD_FIL:30
for M being Aleph st M is strongly_inaccessible holds
M is inaccessible ;

registration
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
b1 is inaccessible
;
end;

theorem :: CARD_FIL:31
for M being Aleph st GCH & M is inaccessible holds
M is strongly_inaccessible by Th28;

definition
let M be Aleph;
attr M is measurable means :: 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 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;
coherence
not nextcard M is limit_cardinal
;
end;

registration
existence
ex b1 being Cardinal st
( not b1 is limit_cardinal & b1 is infinite )
proof end;
end;

registration
cluster non finite cardinal non limit_cardinal -> regular for set ;
coherence
for b1 being Aleph st not b1 is limit_cardinal holds
b1 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 b1 being Cardinal st M = nextcard b1
by CARD_1:def 4;
uniqueness
for b1, b2 being Cardinal st M = nextcard b1 & M = nextcard b2 holds
b1 = b2
by CARD_3:89;
end;

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

registration
let M be non limit_cardinal Aleph;
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 (),M,(bool M);
pred T is_Ulam_Matrix_of M means :: 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 defines is_Ulam_Matrix_of CARD_FIL:def 18 :
for M being non limit_cardinal Aleph
for T being Inf_Matrix of (),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 ) ) );

:: this is pretty long
theorem Th34: :: CARD_FIL:34
for M being non limit_cardinal Aleph ex T being Inf_Matrix of (),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 by ;

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