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₁[ 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₁[x,Z] )

proof

let x be object ; :: thesis: ( x in X implies ex Z being object st
( Z in F & S₁[x,Z] ) )
assume x in X ; :: thesis: ex Z being object st
( Z in F & S₁[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₁[x,Z] ; :: thesis: contradiction
not X \ {x} in F

proof

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 A5: {x} in F by A1, A3;
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;

consider h being Function such that
A6: dom h = X and
rng h c= F and
A7: for x being object st x in X holds
S₁[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

proof

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₁[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;

for y being object holds not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )

proof

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

now :: thesis: not y in h . y

assume A15: y in h . y ; :: thesis: contradiction
S₁[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;

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

end;

then A17: Y /\ (meet { (h . x) where x is Element of X : x in Y } ) = {} by XBOOLE_0:def 1;
A18: not Y is empty by A9, Def1;
A19: not { (h . x) where x is Element of X : x in Y } is empty

proof

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;

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

proof

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;

then A20: card { (h . x) where x is Element of X : x in Y } c= card Y by CARD_1:66;
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