# Metamath Proof Explorer

## Theorem ofrfval

Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses offval.1 ${⊢}{\phi }\to {F}Fn{A}$
offval.2 ${⊢}{\phi }\to {G}Fn{B}$
offval.3 ${⊢}{\phi }\to {A}\in {V}$
offval.4 ${⊢}{\phi }\to {B}\in {W}$
offval.5 ${⊢}{A}\cap {B}={S}$
offval.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={C}$
offval.7 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {G}\left({x}\right)={D}$
Assertion ofrfval ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{C}{R}{D}\right)$

### Proof

Step Hyp Ref Expression
1 offval.1 ${⊢}{\phi }\to {F}Fn{A}$
2 offval.2 ${⊢}{\phi }\to {G}Fn{B}$
3 offval.3 ${⊢}{\phi }\to {A}\in {V}$
4 offval.4 ${⊢}{\phi }\to {B}\in {W}$
5 offval.5 ${⊢}{A}\cap {B}={S}$
6 offval.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={C}$
7 offval.7 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {G}\left({x}\right)={D}$
8 fnex ${⊢}\left({F}Fn{A}\wedge {A}\in {V}\right)\to {F}\in \mathrm{V}$
9 1 3 8 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{V}$
10 fnex ${⊢}\left({G}Fn{B}\wedge {B}\in {W}\right)\to {G}\in \mathrm{V}$
11 2 4 10 syl2anc ${⊢}{\phi }\to {G}\in \mathrm{V}$
12 dmeq ${⊢}{f}={F}\to \mathrm{dom}{f}=\mathrm{dom}{F}$
13 dmeq ${⊢}{g}={G}\to \mathrm{dom}{g}=\mathrm{dom}{G}$
14 12 13 ineqan12d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \mathrm{dom}{f}\cap \mathrm{dom}{g}=\mathrm{dom}{F}\cap \mathrm{dom}{G}$
15 fveq1 ${⊢}{f}={F}\to {f}\left({x}\right)={F}\left({x}\right)$
16 fveq1 ${⊢}{g}={G}\to {g}\left({x}\right)={G}\left({x}\right)$
17 15 16 breqan12d ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left({f}\left({x}\right){R}{g}\left({x}\right)↔{F}\left({x}\right){R}{G}\left({x}\right)\right)$
18 14 17 raleqbidv ${⊢}\left({f}={F}\wedge {g}={G}\right)\to \left(\forall {x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){R}{g}\left({x}\right)↔\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\right)$
19 df-ofr ${⊢}{\circ }_{r}{R}=\left\{⟨{f},{g}⟩|\forall {x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){R}{g}\left({x}\right)\right\}$
20 18 19 brabga ${⊢}\left({F}\in \mathrm{V}\wedge {G}\in \mathrm{V}\right)\to \left({F}{{R}}_{f}{G}↔\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\right)$
21 9 11 20 syl2anc ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}↔\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\right)$
22 1 fndmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
23 2 fndmd ${⊢}{\phi }\to \mathrm{dom}{G}={B}$
24 22 23 ineq12d ${⊢}{\phi }\to \mathrm{dom}{F}\cap \mathrm{dom}{G}={A}\cap {B}$
25 24 5 syl6eq ${⊢}{\phi }\to \mathrm{dom}{F}\cap \mathrm{dom}{G}={S}$
26 25 raleqdv ${⊢}{\phi }\to \left(\forall {x}\in \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)\right)$
27 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
28 5 27 eqsstrri ${⊢}{S}\subseteq {A}$
29 28 sseli ${⊢}{x}\in {S}\to {x}\in {A}$
30 29 6 sylan2 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {F}\left({x}\right)={C}$
31 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
32 5 31 eqsstrri ${⊢}{S}\subseteq {B}$
33 32 sseli ${⊢}{x}\in {S}\to {x}\in {B}$
34 33 7 sylan2 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {G}\left({x}\right)={D}$
35 30 34 breq12d ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to \left({F}\left({x}\right){R}{G}\left({x}\right)↔{C}{R}{D}\right)$
36 35 ralbidva ${⊢}{\phi }\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){R}{G}\left({x}\right)↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{C}{R}{D}\right)$
37 21 26 36 3bitrd ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{C}{R}{D}\right)$