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 )
assume A1: ( not F is principal & F is being_ultrafilter ) ; :: thesis: ( not F is_complete_with card X or F is uniform )
assume A2: 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
A3: ( Y in F & not card Y = card X ) by Def5;
A4: not Y is empty by A3, Def1;
defpred S₁[ set , set ] means ( not $1 in $2 & $2 in F );
A5: for x being set st x in X holds
ex Z being set st
( Z in F & S₁[x,Z] )

proof

let x be set ; :: thesis: ( x in X implies ex Z being set st
( Z in F & S₁[x,Z] ) )
assume A6: x in X ; :: thesis: ex Z being set st
( Z in F & S₁[x,Z] )
A7: {x} is Subset of X by A6, SUBSET_1:55;
assume A8: for Z being set holds
( not Z in F or x in Z or not Z in F ) ; :: thesis: contradiction
A9: for Z being Subset of X st Z in F holds
{x} c= Z

proof

let Z be Subset of X; :: thesis: ( Z in F implies {x} c= Z )
assume A10: Z in F ; :: thesis: {x} c= Z
x in Z by A8, A10;
hence {x} c= Z by ZFMISC_1:37; :: thesis: verum

end;

not X \ {x} in F

proof

assume X \ {x} in F ; :: thesis: contradiction
then x in X \ {x} by A8;
then not x in {x} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then {x} in F by A1, A7, Def7;
hence contradiction by A1, A9, Def6; :: thesis: verum

end;

consider h being Function such that
A11: dom h = X and
rng h c= F and
A12: for x being set st x in X holds
S₁[x,h . x] from WELLORD2:sch 1(A5);
A13: { (h . x) where x is Element of X : x in Y } c= F

proof

let y be set ; :: 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 A14: y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in F
consider x being Element of X such that
A15: y = h . x and
x in Y by A14;
thus y in F by A12, A15; :: thesis: verum

end;

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

proof

consider y being Element of Y;
y in Y by A4;
then h . 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 set ; :: 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 A17: y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in h .: Y
consider x being Element of X such that
A18: y = h . x and
A19: x in Y by A17;
thus y in h .: Y by A11, A18, A19, FUNCT_1:def 12; :: thesis: verum

end;

then A20: card { (h . x) where x is Element of X : x in Y } c= card Y by CARD_2:2;
card Y c= card X by CARD_1:27;
then card Y in card X by A3, CARD_1:13;
then card { (h . x) where x is Element of X : x in Y } in card X by A20, ORDINAL1:22;
then A21: meet { (h . x) where x is Element of X : x in Y } in F by A2, A13, A16, Def3;
for y being set holds not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )

proof

let y be set ; :: thesis: not y in Y /\ (meet { (h . x) where x is Element of X : x in Y } )
assume A22: y in Y /\ (meet { (h . x) where x is Element of X : x in Y } ) ; :: thesis: contradiction
A23: y in Y by A22, XBOOLE_0:def 4;
A24: not y in h . y by A12, A22;
h . y in { (h . x) where x is Element of X : x in Y } by A23;
then not y in meet { (h . x) where x is Element of X : x in Y } by A24, SETFAM_1:def 1;
hence contradiction by A22, XBOOLE_0:def 4; :: thesis: verum

end;

then Y /\ (meet { (h . x) where x is Element of X : x in Y } ) = {} by XBOOLE_0:def 1;
then {} in F by A3, A21, Def1;
hence contradiction by Def1; :: thesis: verum