# Metamath Proof Explorer

## Theorem offval2

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

Ref Expression
Hypotheses offval2.1 ${⊢}{\phi }\to {A}\in {V}$
offval2.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {W}$
offval2.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {X}$
offval2.4 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
offval2.5 ${⊢}{\phi }\to {G}=\left({x}\in {A}⟼{C}\right)$
Assertion offval2 ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({x}\in {A}⟼{B}{R}{C}\right)$

### Proof

Step Hyp Ref Expression
1 offval2.1 ${⊢}{\phi }\to {A}\in {V}$
2 offval2.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {W}$
3 offval2.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {X}$
4 offval2.4 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
5 offval2.5 ${⊢}{\phi }\to {G}=\left({x}\in {A}⟼{C}\right)$
6 2 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}$
7 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
8 7 fnmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\to \left({x}\in {A}⟼{B}\right)Fn{A}$
9 6 8 syl ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)Fn{A}$
10 4 fneq1d ${⊢}{\phi }\to \left({F}Fn{A}↔\left({x}\in {A}⟼{B}\right)Fn{A}\right)$
11 9 10 mpbird ${⊢}{\phi }\to {F}Fn{A}$
12 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {X}$
13 eqid ${⊢}\left({x}\in {A}⟼{C}\right)=\left({x}\in {A}⟼{C}\right)$
14 13 fnmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {X}\to \left({x}\in {A}⟼{C}\right)Fn{A}$
15 12 14 syl ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)Fn{A}$
16 5 fneq1d ${⊢}{\phi }\to \left({G}Fn{A}↔\left({x}\in {A}⟼{C}\right)Fn{A}\right)$
17 15 16 mpbird ${⊢}{\phi }\to {G}Fn{A}$
18 inidm ${⊢}{A}\cap {A}={A}$
19 4 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}=\left({x}\in {A}⟼{B}\right)$
20 19 fveq1d ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {F}\left({y}\right)=\left({x}\in {A}⟼{B}\right)\left({y}\right)$
21 5 adantr ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}=\left({x}\in {A}⟼{C}\right)$
22 21 fveq1d ${⊢}\left({\phi }\wedge {y}\in {A}\right)\to {G}\left({y}\right)=\left({x}\in {A}⟼{C}\right)\left({y}\right)$
23 11 17 1 1 18 20 22 offval ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({y}\in {A}⟼\left({x}\in {A}⟼{B}\right)\left({y}\right){R}\left({x}\in {A}⟼{C}\right)\left({y}\right)\right)$
24 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
25 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{R}$
26 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{C}\right)\left({y}\right)$
27 24 25 26 nfov ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}⟼{B}\right)\left({y}\right){R}\left({x}\in {A}⟼{C}\right)\left({y}\right)\right)$
28 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}⟼{B}\right)\left({x}\right){R}\left({x}\in {A}⟼{C}\right)\left({x}\right)\right)$
29 fveq2 ${⊢}{y}={x}\to \left({x}\in {A}⟼{B}\right)\left({y}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
30 fveq2 ${⊢}{y}={x}\to \left({x}\in {A}⟼{C}\right)\left({y}\right)=\left({x}\in {A}⟼{C}\right)\left({x}\right)$
31 29 30 oveq12d ${⊢}{y}={x}\to \left({x}\in {A}⟼{B}\right)\left({y}\right){R}\left({x}\in {A}⟼{C}\right)\left({y}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right){R}\left({x}\in {A}⟼{C}\right)\left({x}\right)$
32 27 28 31 cbvmpt ${⊢}\left({y}\in {A}⟼\left({x}\in {A}⟼{B}\right)\left({y}\right){R}\left({x}\in {A}⟼{C}\right)\left({y}\right)\right)=\left({x}\in {A}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right){R}\left({x}\in {A}⟼{C}\right)\left({x}\right)\right)$
33 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
34 7 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in {W}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
35 33 2 34 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
36 13 fvmpt2 ${⊢}\left({x}\in {A}\wedge {C}\in {X}\right)\to \left({x}\in {A}⟼{C}\right)\left({x}\right)={C}$
37 33 3 36 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{C}\right)\left({x}\right)={C}$
38 35 37 oveq12d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right){R}\left({x}\in {A}⟼{C}\right)\left({x}\right)={B}{R}{C}$
39 38 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼\left({x}\in {A}⟼{B}\right)\left({x}\right){R}\left({x}\in {A}⟼{C}\right)\left({x}\right)\right)=\left({x}\in {A}⟼{B}{R}{C}\right)$
40 32 39 syl5eq ${⊢}{\phi }\to \left({y}\in {A}⟼\left({x}\in {A}⟼{B}\right)\left({y}\right){R}\left({x}\in {A}⟼{C}\right)\left({y}\right)\right)=\left({x}\in {A}⟼{B}{R}{C}\right)$
41 23 40 eqtrd ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({x}\in {A}⟼{B}{R}{C}\right)$