# Metamath Proof Explorer

## Theorem ofmres

Description: Equivalent expressions for a restriction of the function operation map. Unlike oF R which is a proper class,  ( oF R |( A X. B ) ) can be a set by ofmresex , allowing it to be used as a function or structure argument. By ofmresval , the restricted operation map values are the same as the original values, allowing theorems for oF R to be reused. (Contributed by NM, 20-Oct-2014)

Ref Expression
Assertion ofmres ${⊢}{{\circ }_{f}{R}↾}_{\left({A}×{B}\right)}=\left({f}\in {A},{g}\in {B}⟼{f}{{R}}_{f}{g}\right)$

### Proof

Step Hyp Ref Expression
1 ssv ${⊢}{A}\subseteq \mathrm{V}$
2 ssv ${⊢}{B}\subseteq \mathrm{V}$
3 resmpo ${⊢}\left({A}\subseteq \mathrm{V}\wedge {B}\subseteq \mathrm{V}\right)\to {\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)↾}_{\left({A}×{B}\right)}=\left({f}\in {A},{g}\in {B}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$
4 1 2 3 mp2an ${⊢}{\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)↾}_{\left({A}×{B}\right)}=\left({f}\in {A},{g}\in {B}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$
5 df-of ${⊢}{\circ }_{f}{R}=\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$
6 5 reseq1i ${⊢}{{\circ }_{f}{R}↾}_{\left({A}×{B}\right)}={\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)↾}_{\left({A}×{B}\right)}$
7 eqid ${⊢}{A}={A}$
8 eqid ${⊢}{B}={B}$
9 vex ${⊢}{f}\in \mathrm{V}$
10 vex ${⊢}{g}\in \mathrm{V}$
11 9 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
12 11 inex1 ${⊢}\mathrm{dom}{f}\cap \mathrm{dom}{g}\in \mathrm{V}$
13 12 mptex ${⊢}\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\in \mathrm{V}$
14 5 ovmpt4g ${⊢}\left({f}\in \mathrm{V}\wedge {g}\in \mathrm{V}\wedge \left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\in \mathrm{V}\right)\to {f}{{R}}_{f}{g}=\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)$
15 9 10 13 14 mp3an ${⊢}{f}{{R}}_{f}{g}=\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)$
16 7 8 15 mpoeq123i ${⊢}\left({f}\in {A},{g}\in {B}⟼{f}{{R}}_{f}{g}\right)=\left({f}\in {A},{g}\in {B}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$
17 4 6 16 3eqtr4i ${⊢}{{\circ }_{f}{R}↾}_{\left({A}×{B}\right)}=\left({f}\in {A},{g}\in {B}⟼{f}{{R}}_{f}{g}\right)$