let x, y be set ; for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds
( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z )
let F, Ch be Function; ( not (dom F) /\ (Ch " {x}) is empty implies ( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) )
assume A1:
not (dom F) /\ (Ch " {x}) is empty
; ( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds
y in F . z )
thus
( y in Intersection (F,Ch,x) implies for z being set st z in dom Ch & Ch . z = x holds
y in F . z )
by Def2; ( ( for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) implies y in Intersection (F,Ch,x) )
thus
( ( for z being set st z in dom Ch & Ch . z = x holds
y in F . z ) implies y in Intersection (F,Ch,x) )
verumproof
consider z being
object such that A2:
z in (dom F) /\ (Ch " {x})
by A1;
A3:
z in Ch " {x}
by A2, XBOOLE_0:def 4;
then
Ch . z in {x}
by FUNCT_1:def 7;
then A4:
Ch . z = x
by TARSKI:def 1;
z in dom F
by A2, XBOOLE_0:def 4;
then A5:
F . z in rng F
by FUNCT_1:def 3;
assume A6:
for
z being
set st
z in dom Ch &
Ch . z = x holds
y in F . z
;
y in Intersection (F,Ch,x)
z in dom Ch
by A3, FUNCT_1:def 7;
then
y in F . z
by A6, A4;
then
y in union (rng F)
by A5, TARSKI:def 4;
hence
y in Intersection (
F,
Ch,
x)
by A6, Def2;
verum
end;