# Metamath Proof Explorer

## Theorem offval22

Description: The function operation expressed as a mapping, variation of offval2 . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses offval22.a ${⊢}{\phi }\to {A}\in {V}$
offval22.b ${⊢}{\phi }\to {B}\in {W}$
offval22.c ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {C}\in {X}$
offval22.d ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {D}\in {Y}$
offval22.f ${⊢}{\phi }\to {F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
offval22.g ${⊢}{\phi }\to {G}=\left({x}\in {A},{y}\in {B}⟼{D}\right)$
Assertion offval22 ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({x}\in {A},{y}\in {B}⟼{C}{R}{D}\right)$

### Proof

Step Hyp Ref Expression
1 offval22.a ${⊢}{\phi }\to {A}\in {V}$
2 offval22.b ${⊢}{\phi }\to {B}\in {W}$
3 offval22.c ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {C}\in {X}$
4 offval22.d ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {D}\in {Y}$
5 offval22.f ${⊢}{\phi }\to {F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
6 offval22.g ${⊢}{\phi }\to {G}=\left({x}\in {A},{y}\in {B}⟼{D}\right)$
7 1 2 xpexd ${⊢}{\phi }\to {A}×{B}\in \mathrm{V}$
8 xp1st ${⊢}{z}\in \left({A}×{B}\right)\to {1}^{st}\left({z}\right)\in {A}$
9 xp2nd ${⊢}{z}\in \left({A}×{B}\right)\to {2}^{nd}\left({z}\right)\in {B}$
10 8 9 jca ${⊢}{z}\in \left({A}×{B}\right)\to \left({1}^{st}\left({z}\right)\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)$
11 fvex ${⊢}{2}^{nd}\left({z}\right)\in \mathrm{V}$
12 fvex ${⊢}{1}^{st}\left({z}\right)\in \mathrm{V}$
13 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{2}^{nd}\left({z}\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{2}^{nd}\left({z}\right)$
15 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{1}^{st}\left({z}\right)$
16 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {x}\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)$
17 nfcsb1v
18 17 nfel1
19 16 18 nfim
20 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {1}^{st}\left({z}\right)\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)$
21 nfcsb1v
22 21 nfel1
23 20 22 nfim
24 eleq1 ${⊢}{y}={2}^{nd}\left({z}\right)\to \left({y}\in {B}↔{2}^{nd}\left({z}\right)\in {B}\right)$
25 24 3anbi3d ${⊢}{y}={2}^{nd}\left({z}\right)\to \left(\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)↔\left({\phi }\wedge {x}\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)\right)$
26 csbeq1a
27 26 eleq1d
28 25 27 imbi12d
29 eleq1 ${⊢}{x}={1}^{st}\left({z}\right)\to \left({x}\in {A}↔{1}^{st}\left({z}\right)\in {A}\right)$
30 29 3anbi2d ${⊢}{x}={1}^{st}\left({z}\right)\to \left(\left({\phi }\wedge {x}\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)↔\left({\phi }\wedge {1}^{st}\left({z}\right)\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)\right)$
31 csbeq1a
32 31 eleq1d
33 30 32 imbi12d
34 3 elexd ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {C}\in \mathrm{V}$
35 13 14 15 19 23 28 33 34 vtocl2gf
36 11 12 35 mp2an
37 36 3expb
38 10 37 sylan2
39 nfcsb1v
40 39 nfel1
41 16 40 nfim
42 nfcsb1v
43 42 nfel1
44 20 43 nfim
45 csbeq1a
46 45 eleq1d
47 25 46 imbi12d
48 csbeq1a
49 48 eleq1d
50 30 49 imbi12d
51 4 elexd ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {D}\in \mathrm{V}$
52 13 14 15 41 44 47 50 51 vtocl2gf
53 11 12 52 mp2an
54 53 3expb
55 10 54 sylan2
56 mpompts
57 5 56 syl6eq
58 mpompts
59 6 58 syl6eq
60 7 38 55 57 59 offval2
61 csbov12g
62 61 csbeq2dv
63 11 62 ax-mp
64 csbov12g
65 12 64 ax-mp
66 63 65 eqtr2i
67 66 mpteq2i
68 mpompts
69 67 68 eqtr4i
70 60 69 syl6eq ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({x}\in {A},{y}\in {B}⟼{C}{R}{D}\right)$