let Omega be non empty set ; for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection X,f)
let f be SetSequence of Omega; for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection X,f)
let X be Subset of Omega; X /\ (Union f) = Union (seqIntersection X,f)
A1:
dom f = NAT
by FUNCT_2:def 1;
now reconsider g =
seqIntersection X,
f as
SetSequence of
Omega ;
let z be
set ;
( z in Union (seqIntersection X,f) implies z in X /\ (Union f) )assume
z in Union (seqIntersection X,f)
;
z in X /\ (Union f)then consider u being
set such that A2:
z in u
and A3:
u in rng g
by TARSKI:def 4;
consider v being
set such that A4:
v in dom g
and A5:
u = g . v
by A3, FUNCT_1:def 5;
reconsider n =
v as
Element of
NAT by A4, FUNCT_2:def 1;
A6:
z in X /\ (f . n)
by A2, A5, Def2;
then A7:
z in X
by XBOOLE_0:def 4;
A8:
f . n in rng f
by A1, FUNCT_1:def 5;
z in f . n
by A6, XBOOLE_0:def 4;
then
z in Union f
by A8, TARSKI:def 4;
hence
z in X /\ (Union f)
by A7, XBOOLE_0:def 4;
verum end;
then A9:
Union (seqIntersection X,f) c= X /\ (Union f)
by TARSKI:def 3;
A10:
dom (seqIntersection X,f) = NAT
by FUNCT_2:def 1;
now let z be
set ;
( z in X /\ (Union f) implies z in Union (seqIntersection X,f) )assume A11:
z in X /\ (Union f)
;
z in Union (seqIntersection X,f)then
z in union (rng f)
by XBOOLE_0:def 4;
then consider u being
set such that A12:
z in u
and A13:
u in rng f
by TARSKI:def 4;
consider v being
set such that A14:
v in dom f
and A15:
u = f . v
by A13, FUNCT_1:def 5;
reconsider n =
v as
Element of
NAT by A14, FUNCT_2:def 1;
X /\ (f . n) = (seqIntersection X,f) . n
by Def2;
then A16:
X /\ (f . n) in rng (seqIntersection X,f)
by A10, FUNCT_1:def 5;
z in X
by A11, XBOOLE_0:def 4;
then
z in X /\ (f . n)
by A12, A15, XBOOLE_0:def 4;
hence
z in Union (seqIntersection X,f)
by A16, TARSKI:def 4;
verum end;
then
X /\ (Union f) c= Union (seqIntersection X,f)
by TARSKI:def 3;
hence
X /\ (Union f) = Union (seqIntersection X,f)
by A9, XBOOLE_0:def 10; verum