let x, y be set ; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( 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; :: thesis: ( ( 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 )
:: thesis: verumproof
assume A2:
for
z being
set st
z in dom Ch &
Ch . z = x holds
y in F . z
;
:: thesis: y in Intersection F,Ch,x
consider z being
set such that A3:
z in (dom F) /\ (Ch " {x})
by A1, XBOOLE_0:def 1;
z in Ch " {x}
by A3, XBOOLE_0:def 4;
then
(
z in dom Ch &
Ch . z in {x} )
by FUNCT_1:def 13;
then
(
z in dom F &
z in dom Ch &
Ch . z = x )
by A3, TARSKI:def 1, XBOOLE_0:def 4;
then
(
F . z in rng F &
y in F . z )
by A2, FUNCT_1:def 5;
then
y in union (rng F)
by TARSKI:def 4;
hence
y in Intersection F,
Ch,
x
by A2, Def2;
:: thesis: verum
end;