let X be non empty set ; :: thesis: for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
let F be Filter of X; :: thesis: ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
set LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;
A1: F in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ;
{ S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } c= Filters X
proof
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
let F2 be object ; :: according to TARSKI:def 3 :: thesis: ( not F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } or F2 in Filters X )
reconsider FF = F2 as set by TARSKI:1;
assume F2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } ; :: thesis: F2 in Filters X
then A2: FF in { S where S is Subset-Family of X : S1[S] } ;
S1[FF] from CARD_FIL:sch 1(A2);
hence F2 in Filters X ; :: thesis: verum
end;
then reconsider LargerF = { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } as non empty Subset of (Filters X) by A1;
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
for Z being set st Z c= LargerF & Z is c=-linear holds
ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let X1 be set ; :: thesis: ( X1 c= LargerF & X1 is c=-linear implies ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) ) )
assume that
A3: X1 c= LargerF and
A4: X1 is c=-linear ; :: thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
per cases ( X1 = {} or not X1 is empty ) ;
suppose A5: X1 = {} ; :: thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
take F ; :: thesis: ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) )
thus ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) ) by A5; :: thesis: verum
end;
suppose not X1 is empty ; :: thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
then reconsider X2 = X1 as non empty Subset of (Filters X) by A3, XBOOLE_1:1;
A6: F c= union X2
proof
defpred S2[ set ] means ( F c= $1 & $1 is Filter of X );
consider F1 being object such that
A7: F1 in X2 by XBOOLE_0:def 1;
reconsider F1 = F1 as set by TARSKI:1;
A8: F1 in { S where S is Subset-Family of X : S2[S] } by A3, A7;
A9: S2[F1] from CARD_FIL:sch 1(A8);
F1 c= union X2 by A7, ZFMISC_1:74;
hence F c= union X2 by A9; :: thesis: verum
end;
union X2 is Filter of X by A4, Th16;
then union X2 in { S where S is Subset-Family of X : ( F c= S & S is Filter of X ) } by A6;
then reconsider MF = union X2 as Element of LargerF ;
take MF ; :: thesis: ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) )
thus ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) ) by ZFMISC_1:74; :: thesis: verum
end;
end;
end;
then consider Uf1 being set such that
A10: Uf1 in LargerF and
A11: for Z being set st Z in LargerF & Z <> Uf1 holds
not Uf1 c= Z by ORDERS_1:65;
reconsider Uf1 = Uf1 as Element of LargerF by A10;
reconsider Uf = Uf1 as Filter of X by Th15;
take Uf ; :: thesis: ( F c= Uf & Uf is being_ultrafilter )
A12: Uf in { S where S is Subset-Family of X : S1[S] } ;
A13: S1[Uf] from CARD_FIL:sch 1(A12);
hence F c= Uf ; :: thesis: Uf is being_ultrafilter
thus Uf is being_ultrafilter :: thesis: verum
proof
let Z be Subset of X; :: according to CARD_FIL:def 7 :: thesis: ( Z in Uf or X \ Z in Uf )
per cases ( Z in Uf or not Z in Uf ) ;
suppose Z in Uf ; :: thesis: ( Z in Uf or X \ Z in Uf )
hence ( Z in Uf or X \ Z in Uf ) ; :: thesis: verum
end;
suppose A14: not Z in Uf ; :: thesis: ( Z in Uf or X \ Z in Uf )
X \ Z in Uf
proof
assume A15: not X \ Z in Uf ; :: thesis: contradiction
A16: for Y1 being Subset of X st Y1 in Uf holds
Y1 meets Z
proof
let Y1 be Subset of X; :: thesis: ( Y1 in Uf implies Y1 meets Z )
assume A17: Y1 in Uf ; :: thesis: Y1 meets Z
assume Y1 misses Z ; :: thesis: contradiction
then Y1 = Y1 \ Z by XBOOLE_1:83;
then Y1 c= X \ Z by XBOOLE_1:33;
hence contradiction by A15, A17, Def1; :: thesis: verum
end;
then A18: Extend_Filter (Uf,Z) is Filter of X by Th14;
A19: Z in Extend_Filter (Uf,Z) by A16, Th14;
A20: Uf c= Extend_Filter (Uf,Z) by A16, Th14;
then F c= Extend_Filter (Uf,Z) by A13;
then Extend_Filter (Uf,Z) in LargerF by A18;
hence contradiction by A11, A14, A20, A19; :: thesis: verum
end;
hence ( Z in Uf or X \ Z in Uf ) ; :: thesis: verum
end;
end;
end;