let X be non empty set ; :: thesis: for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
let FS be non empty Subset of (Filters X); :: thesis: ( FS is c=-linear implies union FS is Filter of X )
A1: for S being set st S in FS holds
S c= bool X
proof
let S be set ; :: thesis: ( S in FS implies S c= bool X )
assume S in FS ; :: thesis: S c= bool X
then S is Element of Filters X ;
hence S c= bool X ; :: thesis: verum
end;
consider S being object such that
A2: S in FS by XBOOLE_0:def 1;
assume A3: FS is c=-linear ; :: thesis: union FS is Filter of X
A4: for Y1, Y2 being Subset of X holds
( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
proof
let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
thus ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) :: thesis: ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS )
proof
assume that
A5: Y1 in union FS and
A6: Y2 in union FS ; :: thesis: Y1 /\ Y2 in union FS
consider S1 being set such that
A7: Y1 in S1 and
A8: S1 in FS by A5, TARSKI:def 4;
A9: S1 is Filter of X by A8, Th15;
consider S2 being set such that
A10: Y2 in S2 and
A11: S2 in FS by A6, TARSKI:def 4;
A12: S1,S2 are_c=-comparable by A3, A8, A11;
A13: S2 is Filter of X by A11, Th15;
per cases ( S1 c= S2 or S2 c= S1 ) by A12;
suppose S2 c= S1 ; :: thesis: Y1 /\ Y2 in union FS
then Y1 /\ Y2 in S1 by A7, A10, A9, Def1;
hence Y1 /\ Y2 in union FS by A8, TARSKI:def 4; :: thesis: verum
end;
end;
end;
assume that
A14: Y1 in union FS and
A15: Y1 c= Y2 ; :: thesis: Y2 in union FS
consider S1 being set such that
A16: Y1 in S1 and
A17: S1 in FS by A14, TARSKI:def 4;
S1 is Filter of X by A17, Th15;
then Y2 in S1 by A15, A16, Def1;
hence Y2 in union FS by A17, TARSKI:def 4; :: thesis: verum
end;
A18: not {} in union FS
proof
assume {} in union FS ; :: thesis: contradiction
then consider S being set such that
A19: {} in S and
A20: S in FS by TARSKI:def 4;
S is Filter of X by A20, Th15;
hence contradiction by A19, Def1; :: thesis: verum
end;
reconsider S = S as set by TARSKI:1;
S is Filter of X by A2, Th15;
then X in S by Th5;
then union FS is non empty Subset-Family of X by A1, A2, TARSKI:def 4, ZFMISC_1:76;
hence union FS is Filter of X by A18, A4, Def1; :: thesis: verum