# Metamath Proof Explorer

## Theorem off

Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses off.1 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {T}\right)\right)\to {x}{R}{y}\in {U}$
off.2 ${⊢}{\phi }\to {F}:{A}⟶{S}$
off.3 ${⊢}{\phi }\to {G}:{B}⟶{T}$
off.4 ${⊢}{\phi }\to {A}\in {V}$
off.5 ${⊢}{\phi }\to {B}\in {W}$
off.6 ${⊢}{A}\cap {B}={C}$
Assertion off ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}\right):{C}⟶{U}$

### Proof

Step Hyp Ref Expression
1 off.1 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {T}\right)\right)\to {x}{R}{y}\in {U}$
2 off.2 ${⊢}{\phi }\to {F}:{A}⟶{S}$
3 off.3 ${⊢}{\phi }\to {G}:{B}⟶{T}$
4 off.4 ${⊢}{\phi }\to {A}\in {V}$
5 off.5 ${⊢}{\phi }\to {B}\in {W}$
6 off.6 ${⊢}{A}\cap {B}={C}$
7 2 ffnd ${⊢}{\phi }\to {F}Fn{A}$
8 3 ffnd ${⊢}{\phi }\to {G}Fn{B}$
9 eqidd ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to {F}\left({z}\right)={F}\left({z}\right)$
10 eqidd ${⊢}\left({\phi }\wedge {z}\in {B}\right)\to {G}\left({z}\right)={G}\left({z}\right)$
11 7 8 4 5 6 9 10 offval ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({z}\in {C}⟼{F}\left({z}\right){R}{G}\left({z}\right)\right)$
12 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
13 6 12 eqsstrri ${⊢}{C}\subseteq {A}$
14 13 sseli ${⊢}{z}\in {C}\to {z}\in {A}$
15 ffvelrn ${⊢}\left({F}:{A}⟶{S}\wedge {z}\in {A}\right)\to {F}\left({z}\right)\in {S}$
16 2 14 15 syl2an ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to {F}\left({z}\right)\in {S}$
17 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
18 6 17 eqsstrri ${⊢}{C}\subseteq {B}$
19 18 sseli ${⊢}{z}\in {C}\to {z}\in {B}$
20 ffvelrn ${⊢}\left({G}:{B}⟶{T}\wedge {z}\in {B}\right)\to {G}\left({z}\right)\in {T}$
21 3 19 20 syl2an ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to {G}\left({z}\right)\in {T}$
22 1 ralrimivva ${⊢}{\phi }\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{x}{R}{y}\in {U}$
23 22 adantr ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{x}{R}{y}\in {U}$
24 ovrspc2v ${⊢}\left(\left({F}\left({z}\right)\in {S}\wedge {G}\left({z}\right)\in {T}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {T}\phantom{\rule{.4em}{0ex}}{x}{R}{y}\in {U}\right)\to {F}\left({z}\right){R}{G}\left({z}\right)\in {U}$
25 16 21 23 24 syl21anc ${⊢}\left({\phi }\wedge {z}\in {C}\right)\to {F}\left({z}\right){R}{G}\left({z}\right)\in {U}$
26 11 25 fmpt3d ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}\right):{C}⟶{U}$