:: by Josef Urban

::

:: Received April 14, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

theorem :: CARD_FIL:1

:: 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} ) ) ) )

( {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 ;

ex b_{1} being non empty Subset-Family of X st

( not {} in b_{1} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in b_{1} & Y2 in b_{1} implies Y1 /\ Y2 in b_{1} ) & ( Y1 in b_{1} & Y1 c= Y2 implies Y2 in b_{1} ) ) ) )

end;
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 ( 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 ) ) ) );

ex b

( not {} in b

( ( Y1 in b

proof end;

:: deftheorem Def1 defines Filter CARD_FIL:def 1 :

for X being non empty set

for b_{2} being non empty Subset-Family of X holds

( b_{2} is Filter of X iff ( not {} in b_{2} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in b_{2} & Y2 in b_{2} implies Y1 /\ Y2 in b_{2} ) & ( Y1 in b_{2} & Y1 c= Y2 implies Y2 in b_{2} ) ) ) ) );

for X being non empty set

for b

( b

( ( Y1 in b

theorem :: CARD_FIL:3

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

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 ) ) ) )

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;

registration

let X be non empty set ;

let S be non empty Subset-Family of X;

coherence

not COMPLEMENT S is empty by SETFAM_1:32;

end;
let S be non empty Subset-Family of X;

coherence

not COMPLEMENT S is empty by SETFAM_1:32;

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 }

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 }

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 ;

ex b_{1} being non empty Subset-Family of X st

( not X in b_{1} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in b_{1} & Y2 in b_{1} implies Y1 \/ Y2 in b_{1} ) & ( Y1 in b_{1} & Y2 c= Y1 implies Y2 in b_{1} ) ) ) )

end;
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 ( 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 ) ) ) );

ex b

( not X in b

( ( Y1 in b

proof end;

:: deftheorem Def2 defines Ideal CARD_FIL:def 2 :

for X being non empty set

for b_{2} being non empty Subset-Family of X holds

( b_{2} is Ideal of X iff ( not X in b_{2} & ( for Y1, Y2 being Subset of X holds

( ( Y1 in b_{2} & Y2 in b_{2} implies Y1 \/ Y2 in b_{2} ) & ( Y1 in b_{2} & Y2 c= Y1 implies Y2 in b_{2} ) ) ) ) );

for X being non empty set

for b

( b

( ( Y1 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

end;
let F be Filter of X;

:: original: dual

redefine func dual F -> Ideal of X;

coherence

dual F is Ideal of X

proof 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 ) ) )

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;

definition

let X be non empty set ;

let N be Cardinal;

let S be non empty Subset-Family of X;

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

for S1 being non empty set st S1 c= S & card S1 in N holds

meet S1 in S;

:: 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 );

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;

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

for S1 being non empty set st S1 c= S & card S1 in N holds

union S1 in S;

:: 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 );

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;
let N be Cardinal;

let F be Filter of X;

synonym F is_complete_with N for F is_multiplicative_with N;

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;
let N be Cardinal;

let I be Ideal of X;

synonym I is_complete_with N for I is_additive_with N;

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

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;

end;
let F be Filter of 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 ) );

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

for Y being Subset of X holds

( Y in F or X \ Y in F );

:: 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 );

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

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

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;

{ 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

end;
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 ) } ;

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

:: 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 ) } ;

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 ) )

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) )

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 ;

{ S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X)

end;
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 } ;

{ S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X)

proof 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 } ;

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

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

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 )

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 ;

{ Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X

end;
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 } ;

{ Y where Y is Subset of X : card (X \ Y) in card X } is Filter of X

proof 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 } ;

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

:: deftheorem defines Frechet_Ideal CARD_FIL:def 11 :

for X being infinite set holds Frechet_Ideal X = dual (Frechet_Filter X);

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 )

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 )

for Y being Subset of X holds

( Y in Frechet_Ideal X iff card Y in card X )

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

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 ;

existence

ex b_{1} being Filter of X st

( not b_{1} is principal & b_{1} is being_ultrafilter )

end;
existence

ex b

( not b

proof end;

registration

let X be infinite set ;

coherence

for b_{1} being Filter of X st b_{1} is uniform & b_{1} is being_ultrafilter holds

not b_{1} is principal

end;
coherence

for b

not b

proof 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 )

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

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;

:: deftheorem defines GCH CARD_FIL:def 12 :

( GCH iff for N being Aleph holds nextcard N = exp (2,N) );

( GCH iff for N being Aleph holds nextcard N = exp (2,N) );

:: deftheorem defines inaccessible CARD_FIL:def 13 :

for IT being Aleph holds

( IT is inaccessible iff ( IT is regular & IT is limit_cardinal ) );

for IT being Aleph holds

( IT is inaccessible iff ( IT is regular & IT is limit_cardinal ) );

registration

coherence

for b_{1} being Aleph st b_{1} is inaccessible holds

( b_{1} is regular & b_{1} is limit_cardinal )
;

end;
for b

( b

definition

let IT be Aleph;

end;
attr IT is strong_limit means :: CARD_FIL:def 14

for N being Cardinal st N in IT holds

exp (2,N) in IT;

for N being Cardinal st N in IT holds

exp (2,N) in IT;

:: 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 );

for IT being Aleph holds

( IT is strong_limit iff for N being Cardinal st N in IT holds

exp (2,N) in IT );

registration
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 ) );

for IT being Aleph holds

( IT is strongly_inaccessible iff ( IT is regular & IT is strong_limit ) );

registration

coherence

for b_{1} being Aleph st b_{1} is strongly_inaccessible holds

( b_{1} is regular & b_{1} is strong_limit )
;

end;
for b

( b

registration
end;

theorem :: CARD_FIL:31

definition

let M be Aleph;

end;
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 );

ex Uf being Filter of M st

( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter );

:: 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 ) );

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

registration
end;

registration
end;

definition

let M be non limit_cardinal Cardinal;

existence

ex b_{1} being Cardinal st M = nextcard b_{1}
by CARD_1:def 4;

uniqueness

for b_{1}, b_{2} being Cardinal st M = nextcard b_{1} & M = nextcard b_{2} holds

b_{1} = b_{2}
by CARD_3:89;

end;
existence

ex b

uniqueness

for b

b

:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :

for M being non limit_cardinal Cardinal

for b_{2} being Cardinal holds

( b_{2} = predecessor M iff M = nextcard b_{2} );

for M being non limit_cardinal Cardinal

for b

( b

registration
end;

definition
end;

definition

let M be non limit_cardinal Aleph;

let T be Inf_Matrix of (predecessor M),M,(bool M);

end;
let T be Inf_Matrix of (predecessor M),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 ) );

( ( 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 ) );

:: deftheorem 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 ) ) );

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

:: this is pretty long

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 ) )

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 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 )

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 :: CARD_FIL:41