let X be set ; :: thesis: for R being non empty Subset-Family of (bool X)
for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds
Intersect F = Intersect (union R)
let R be non empty Subset-Family of (bool X); :: thesis: for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds
Intersect F = Intersect (union R)
let F be Subset-Family of X; :: thesis: ( F = { (Intersect x) where x is Element of R : verum } implies Intersect F = Intersect (union R) )
assume A1: F = { (Intersect x) where x is Element of R : verum } ; :: thesis: Intersect F = Intersect (union R)
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Intersect (union R) c= Intersect F
let c be object ; :: thesis: ( c in Intersect F implies c in Intersect (union R) )
assume A2: c in Intersect F ; :: thesis: c in Intersect (union R)
for Y being set st Y in union R holds
c in Y
proof
let Y be set ; :: thesis: ( Y in union R implies c in Y )
assume Y in union R ; :: thesis: c in Y
then consider d being set such that
A3: Y in d and
A4: d in R by TARSKI:def 4;
reconsider d = d as Subset-Family of X by A4;
reconsider d = d as Subset-Family of X ;
Intersect d in F by A1, A4;
then c in Intersect d by A2, SETFAM_1:43;
hence c in Y by A3, SETFAM_1:43; :: thesis: verum
end;
hence c in Intersect (union R) by A2, SETFAM_1:43; :: thesis: verum
end;
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in Intersect (union R) or c in Intersect F )
assume A5: c in Intersect (union R) ; :: thesis: c in Intersect F
for Y being set st Y in F holds
c in Y
proof
let Y be set ; :: thesis: ( Y in F implies c in Y )
assume Y in F ; :: thesis: c in Y
then consider x being Element of R such that
A6: Y = Intersect x by A1;
Intersect (union R) c= Intersect x by SETFAM_1:44, ZFMISC_1:74;
hence c in Y by A5, A6; :: thesis: verum
end;
hence c in Intersect F by A5, SETFAM_1:43; :: thesis: verum