let y, X9 be set ; for F, Ch being Function holds (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)
let F, Ch be Function; (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)
set I = Intersect (F,((dom F) --> X9));
set Int1 = Intersection (F,Ch,y);
set Int2 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y);
thus
(Intersection (F,Ch,y)) /\ X9 c= Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)
XBOOLE_0:def 10 Intersection ((Intersect (F,((dom F) --> X9))),Ch,y) c= (Intersection (F,Ch,y)) /\ X9proof
let x be
object ;
TARSKI:def 3 ( not x in (Intersection (F,Ch,y)) /\ X9 or x in Intersection ((Intersect (F,((dom F) --> X9))),Ch,y) )
assume A1:
x in (Intersection (F,Ch,y)) /\ X9
;
x in Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)
A2:
for
z being
set st
z in dom Ch &
Ch . z = y holds
x in (Intersect (F,((dom F) --> X9))) . z
proof
A3:
x in Intersection (
F,
Ch,
y)
by A1, XBOOLE_0:def 4;
let z be
set ;
( z in dom Ch & Ch . z = y implies x in (Intersect (F,((dom F) --> X9))) . z )
assume
(
z in dom Ch &
Ch . z = y )
;
x in (Intersect (F,((dom F) --> X9))) . z
then A4:
x in F . z
by A3, Def2;
then A5:
z in dom F
by FUNCT_1:def 2;
x in X9
by A1, XBOOLE_0:def 4;
then
x in (F . z) /\ X9
by A4, XBOOLE_0:def 4;
hence
x in (Intersect (F,((dom F) --> X9))) . z
by A5, Th48;
verum
end;
x in X9
by A1, XBOOLE_0:def 4;
then
x in (union (rng F)) /\ X9
by A1, XBOOLE_0:def 4;
then
x in union (rng (Intersect (F,((dom F) --> X9))))
by Th49;
hence
x in Intersection (
(Intersect (F,((dom F) --> X9))),
Ch,
y)
by A2, Def2;
verum
end;
thus
Intersection ((Intersect (F,((dom F) --> X9))),Ch,y) c= (Intersection (F,Ch,y)) /\ X9
verumproof
let x be
object ;
TARSKI:def 3 ( not x in Intersection ((Intersect (F,((dom F) --> X9))),Ch,y) or x in (Intersection (F,Ch,y)) /\ X9 )
assume A6:
x in Intersection (
(Intersect (F,((dom F) --> X9))),
Ch,
y)
;
x in (Intersection (F,Ch,y)) /\ X9
x in union (rng (Intersect (F,((dom F) --> X9))))
by A6;
then A7:
x in (union (rng F)) /\ X9
by Th49;
then A8:
x in X9
by XBOOLE_0:def 4;
A9:
for
z being
set st
z in dom Ch &
Ch . z = y holds
x in F . z
x in union (rng F)
by A7, XBOOLE_0:def 4;
then
x in Intersection (
F,
Ch,
y)
by A9, Def2;
hence
x in (Intersection (F,Ch,y)) /\ X9
by A8, XBOOLE_0:def 4;
verum
end;