:: CARD_FIL semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X, Y be set ;
:: original: \
redefine func X \ Y -> Subset of X;
coherence
X \ Y is Subset of X
by XBOOLE_1:36;
end;

theorem Th1: :: CARD_FIL:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for X being infinite set holds Card {x} <` Card X
proof end;

registration
let X be infinite set ;
cluster Card X -> infinite ;
coherence
not Card X is finite
by CARD_4:1;
end;

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;

theorem Th2: :: CARD_FIL:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set holds {X} is Filter of X
proof end;

theorem Th5: :: CARD_FIL:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for F being Filter of X holds X in F
proof end;

theorem Th6: :: CARD_FIL:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 <` 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 <` 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 <` 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 <` 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) <` Card X } ;
coherence
{ Y where Y is Subset of X : Card (X \ Y) <` 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) <` 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff Card (X \ Y) <` Card X )
proof end;

theorem Th19: :: CARD_FIL:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Ideal X iff Card Y <` Card X )
proof end;

theorem Th20: :: CARD_FIL:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Cardinal holds nextcard N <=` 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 );
end;

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

notation
let IT be Aleph;
synonym IT is_inaccessible_cardinal for inaccessible IT;
end;

registration
cluster inaccessible -> limit regular set ;
coherence
for b1 being Aleph st b1 is inaccessible holds
( b1 is regular & b1 is limit )
by Def13;
end;

theorem :: CARD_FIL:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
alef 0 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 <` IT holds
exp 2,N <` 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 <` IT holds
exp 2,N <` IT );

notation
let IT be Aleph;
synonym IT is_strong_limit_cardinal for strong_limit IT;
end;

theorem Th26: :: CARD_FIL:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
alef 0 is strong_limit
proof end;

theorem Th27: :: CARD_FIL:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is strong_limit holds
M is limit
proof end;

registration
cluster strong_limit -> limit set ;
coherence
for b1 being Aleph st b1 is strong_limit holds
b1 is limit
by Th27;
end;

theorem Th28: :: CARD_FIL:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st GCH & M is limit 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 ) );

notation
let IT be Aleph;
synonym IT is_strongly_inaccessible_cardinal for strongly_inaccessible IT;
end;

registration
cluster strongly_inaccessible -> limit regular strong_limit set ;
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
( b1 is regular & b1 is strong_limit )
by Def15;
end;

theorem :: CARD_FIL:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
alef 0 is strongly_inaccessible by Def15, Th26, CARD_5:42;

theorem Th30: :: CARD_FIL:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is strongly_inaccessible holds
M is inaccessible
proof end;

registration
cluster strongly_inaccessible -> limit regular inaccessible set ;
coherence
for b1 being Aleph st b1 is strongly_inaccessible holds
b1 is inaccessible
by Th30;
end;

theorem :: CARD_FIL:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) );

notation
let M be Aleph;
synonym M is_measurable_cardinal for measurable M;
end;

theorem Th32: :: CARD_FIL:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is measurable holds
M is regular
proof end;

registration
let M be Aleph;
cluster nextcard M -> non limit ;
coherence
not nextcard M is limit
proof end;
end;

registration
cluster infinite non limit set ;
existence
ex b1 being Cardinal st
( not b1 is limit & not b1 is finite )
proof end;
end;

registration
cluster non limit -> regular set ;
coherence
for b1 being Aleph st not b1 is limit holds
b1 is regular
proof end;
end;

definition
let M be non limit 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 7;
uniqueness
for b1, b2 being Cardinal st M = nextcard b1 & M = nextcard b2 holds
b1 = b2
by CARD_4:21;
end;

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

registration
let M be non limit 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 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 } )) <=` 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 } )) <=` predecessor M ) );
end;

:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def 18 :
for M being non limit 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 } )) <=` 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 } )) <=` predecessor M ) ) );

theorem Th34: :: CARD_FIL:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non limit 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non limit 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for N being Cardinal st N <=` Card X holds
ex Y being set st
( Y c= X & Card Y = N )
proof end;

theorem Th37: :: CARD_FIL:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non limit 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is measurable holds
M is limit
proof end;

theorem :: CARD_FIL:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is measurable holds
M is inaccessible
proof end;

theorem Th40: :: CARD_FIL:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is measurable holds
M is strong_limit
proof end;

theorem :: CARD_FIL:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Aleph st M is measurable holds
M is strongly_inaccessible
proof end;