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₁[ set , set ] means ( not $1 in $2 & $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 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 x in X ; :: thesis: ex Z being set st
( Z in F & S₁[x,Z] )
then A3: {x} is Subset of X by SUBSET_1:55;
assume A4: for Z being set holds
( not Z in F or x in Z or not Z in F ) ; :: 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, Def7;
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 Z in F ; :: thesis: {x} c= Z
then x in Z by A4;
hence {x} c= Z by ZFMISC_1:37; :: thesis: verum

end;

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

end;

consider h being Function such that
A6: dom h = X and
rng h c= F and
A7: for x being set st x in X holds
S₁[x,h . x] from WELLORD2:sch 1(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 by Def5;
A11: { (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 y in { (h . x) where x is Element of X : x in Y } ; :: thesis: y in F
then ex x being Element of X st
( y = h . x & x in Y ) ;
hence y in F by A7; :: thesis: verum

end;

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 A12: y in Y /\ (meet { (h . x) where x is Element of X : x in Y } ) ; :: thesis: contradiction
y in Y by A12, XBOOLE_0:def 4;
then A13: h . y in { (h . x) where x is Element of X : x in Y } ;
not y in h . y by A7, A12;
then not y in meet { (h . x) where x is Element of X : x in Y } by A13, SETFAM_1:def 1;
hence contradiction by A12, XBOOLE_0:def 4; :: thesis: verum

end;

then A14: Y /\ (meet { (h . x) where x is Element of X : x in Y } ) = {} by XBOOLE_0:def 1;
A15: not Y is empty by A9, Def1;
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 A15;
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 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 12; :: thesis: verum

end;

then A17: 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 A10, CARD_1:13;
then card { (h . x) where x is Element of X : x in Y } in card X by A17, ORDINAL1:22;
then meet { (h . x) where x is Element of X : x in Y } in F by A8, A11, A16, Def3;
then {} in F by A9, A14, Def1;
hence contradiction by Def1; :: thesis: verum