let X be infinite set ; :: thesis: 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

let F be Filter of X; :: thesis: ( not F is principal & F is being_ultrafilter & F is_complete_with card X implies F is uniform )

defpred S_{1}[ object , object ] means ex A being set st

( A = $2 & not $1 in A & $2 in F );

assume A1: ( not F is principal & F is being_ultrafilter ) ; :: thesis: ( not F is_complete_with card X or F is uniform )

A2: for x being object st x in X holds

ex Z being object st

( Z in F & S_{1}[x,Z] )

A6: dom h = X and

rng h c= F and

A7: for x being object st x in X holds

S_{1}[x,h . x]
from FUNCT_1:sch 6(A2);

assume A8: F is_complete_with card X ; :: thesis: F is uniform

assume not F is uniform ; :: thesis: contradiction

then consider Y being Subset of X such that

A9: Y in F and

A10: not card Y = card X ;

A11: { (h . x) where x is Element of X : x in Y } c= F

A18: not Y is empty by A9, Def1;

A19: not { (h . x) where x is Element of X : x in Y } is empty

card Y c= card X by CARD_1:11;

then card Y in card X by A10, CARD_1:3;

then card { (h . x) where x is Element of X : x in Y } in card X by A20, ORDINAL1:12;

then meet { (h . x) where x is Element of X : x in Y } in F by A8, A11, A19;

then {} in F by A9, A17, Def1;

hence contradiction by Def1; :: thesis: verum

F is uniform

let F be Filter of X; :: thesis: ( not F is principal & F is being_ultrafilter & F is_complete_with card X implies F is uniform )

defpred S

( A = $2 & not $1 in A & $2 in F );

assume A1: ( not F is principal & F is being_ultrafilter ) ; :: thesis: ( not F is_complete_with card X or F is uniform )

A2: for x being object st x in X holds

ex Z being object st

( Z in F & S

proof

consider h being Function such that
let x be object ; :: thesis: ( x in X implies ex Z being object st

( Z in F & S_{1}[x,Z] ) )

assume x in X ; :: thesis: ex Z being object st

( Z in F & S_{1}[x,Z] )

then A3: {x} is Subset of X by SUBSET_1:33;

assume A4: for Z being object st Z in F holds

not S_{1}[x,Z]
; :: thesis: contradiction

not X \ {x} in F

for Z being Subset of X st Z in F holds

{x} c= Z by A4, ZFMISC_1:31;

hence contradiction by A1, A5; :: thesis: verum

end;( Z in F & S

assume x in X ; :: thesis: ex Z being object st

( Z in F & S

then A3: {x} is Subset of X by SUBSET_1:33;

assume A4: for Z being object st Z in F holds

not S

not X \ {x} in F

proof

then A5:
{x} in F
by A1, A3;
assume
X \ {x} in F
; :: thesis: contradiction

then x in X \ {x} by A4;

then not x in {x} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then x in X \ {x} by A4;

then not x in {x} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

for Z being Subset of X st Z in F holds

{x} c= Z by A4, ZFMISC_1:31;

hence contradiction by A1, A5; :: thesis: verum

A6: dom h = X and

rng h c= F and

A7: for x being object st x in X holds

S

assume A8: F is_complete_with card X ; :: thesis: F is uniform

assume not F is uniform ; :: thesis: contradiction

then consider Y being Subset of X such that

A9: Y in F and

A10: not card Y = card X ;

A11: { (h . x) where x is Element of X : x in Y } c= F

proof

for y being object holds not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (h . x) where x is Element of X : x in Y } or y in F )

assume y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in F

then consider x being Element of X such that

A12: ( y = h . x & x in Y ) ;

S_{1}[x,h . x]
by A7;

then ex B being set st

( B = h . x & not x in B & h . x in F ) ;

hence y in F by A12; :: thesis: verum

end;assume y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in F

then consider x being Element of X such that

A12: ( y = h . x & x in Y ) ;

S

then ex B being set st

( B = h . x & not x in B & h . x in F ) ;

hence y in F by A12; :: thesis: verum

proof

then A17:
Y /\ (meet { (h . x) where x is Element of X : x in Y } ) = {}
by XBOOLE_0:def 1;
let y be object ; :: thesis: not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )

assume A13: y in Y /\ (meet { (h . x) where x is Element of X : x in Y } ) ; :: thesis: contradiction

y in Y by A13, XBOOLE_0:def 4;

then A14: h . y in { (h . x) where x is Element of X : x in Y } ;

hence contradiction by A13, XBOOLE_0:def 4; :: thesis: verum

end;assume A13: y in Y /\ (meet { (h . x) where x is Element of X : x in Y } ) ; :: thesis: contradiction

y in Y by A13, XBOOLE_0:def 4;

then A14: h . y in { (h . x) where x is Element of X : x in Y } ;

now :: thesis: not y in h . y

then
not y in meet { (h . x) where x is Element of X : x in Y }
by A14, SETFAM_1:def 1;assume A15:
y in h . y
; :: thesis: contradiction

S_{1}[y,h . y]
by A7, A13;

then consider A being set such that

A16: ( A = h . y & not y in A & h . y in F ) ;

( not y in h . y & h . y in F ) by A16;

hence contradiction by A15; :: thesis: verum

end;S

then consider A being set such that

A16: ( A = h . y & not y in A & h . y in F ) ;

( not y in h . y & h . y in F ) by A16;

hence contradiction by A15; :: thesis: verum

hence contradiction by A13, XBOOLE_0:def 4; :: thesis: verum

A18: not Y is empty by A9, Def1;

A19: not { (h . x) where x is Element of X : x in Y } is empty

proof

{ (h . x) where x is Element of X : x in Y } c= h .: Y
set y = the Element of Y;

the Element of Y in Y by A18;

then h . the Element of Y in { (h . x) where x is Element of X : x in Y } ;

hence not { (h . x) where x is Element of X : x in Y } is empty ; :: thesis: verum

end;the Element of Y in Y by A18;

then h . the Element of Y in { (h . x) where x is Element of X : x in Y } ;

hence not { (h . x) where x is Element of X : x in Y } is empty ; :: thesis: verum

proof

then A20:
card { (h . x) where x is Element of X : x in Y } c= card Y
by CARD_1:66;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (h . x) where x is Element of X : x in Y } or y in h .: Y )

assume y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in h .: Y

then ex x being Element of X st

( y = h . x & x in Y ) ;

hence y in h .: Y by A6, FUNCT_1:def 6; :: thesis: verum

end;assume y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in h .: Y

then ex x being Element of X st

( y = h . x & x in Y ) ;

hence y in h .: Y by A6, FUNCT_1:def 6; :: thesis: verum

card Y c= card X by CARD_1:11;

then card Y in card X by A10, CARD_1:3;

then card { (h . x) where x is Element of X : x in Y } in card X by A20, ORDINAL1:12;

then meet { (h . x) where x is Element of X : x in Y } in F by A8, A11, A19;

then {} in F by A9, A17, Def1;

hence contradiction by Def1; :: thesis: verum