# Metamath Proof Explorer

## Theorem xpmapenlem

Description: Lemma for xpmapen . (Contributed by NM, 1-May-2004) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses xpmapen.1 ${⊢}{A}\in \mathrm{V}$
xpmapen.2 ${⊢}{B}\in \mathrm{V}$
xpmapen.3 ${⊢}{C}\in \mathrm{V}$
xpmapenlem.4 ${⊢}{D}=\left({z}\in {C}⟼{1}^{st}\left({x}\left({z}\right)\right)\right)$
xpmapenlem.5 ${⊢}{R}=\left({z}\in {C}⟼{2}^{nd}\left({x}\left({z}\right)\right)\right)$
xpmapenlem.6 ${⊢}{S}=\left({z}\in {C}⟼⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)$
Assertion xpmapenlem ${⊢}\left({\left({A}×{B}\right)}^{{C}}\right)\approx \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 xpmapen.1 ${⊢}{A}\in \mathrm{V}$
2 xpmapen.2 ${⊢}{B}\in \mathrm{V}$
3 xpmapen.3 ${⊢}{C}\in \mathrm{V}$
4 xpmapenlem.4 ${⊢}{D}=\left({z}\in {C}⟼{1}^{st}\left({x}\left({z}\right)\right)\right)$
5 xpmapenlem.5 ${⊢}{R}=\left({z}\in {C}⟼{2}^{nd}\left({x}\left({z}\right)\right)\right)$
6 xpmapenlem.6 ${⊢}{S}=\left({z}\in {C}⟼⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)$
7 ovex ${⊢}{\left({A}×{B}\right)}^{{C}}\in \mathrm{V}$
8 ovex ${⊢}{{A}}^{{C}}\in \mathrm{V}$
9 ovex ${⊢}{{B}}^{{C}}\in \mathrm{V}$
10 8 9 xpex ${⊢}\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\in \mathrm{V}$
11 1 2 xpex ${⊢}{A}×{B}\in \mathrm{V}$
12 11 3 elmap ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)↔{x}:{C}⟶{A}×{B}$
13 ffvelrn ${⊢}\left({x}:{C}⟶{A}×{B}\wedge {z}\in {C}\right)\to {x}\left({z}\right)\in \left({A}×{B}\right)$
14 12 13 sylanb ${⊢}\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {z}\in {C}\right)\to {x}\left({z}\right)\in \left({A}×{B}\right)$
15 xp1st ${⊢}{x}\left({z}\right)\in \left({A}×{B}\right)\to {1}^{st}\left({x}\left({z}\right)\right)\in {A}$
16 14 15 syl ${⊢}\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {z}\in {C}\right)\to {1}^{st}\left({x}\left({z}\right)\right)\in {A}$
17 16 4 fmptd ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\to {D}:{C}⟶{A}$
18 1 3 elmap ${⊢}{D}\in \left({{A}}^{{C}}\right)↔{D}:{C}⟶{A}$
19 17 18 sylibr ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\to {D}\in \left({{A}}^{{C}}\right)$
20 xp2nd ${⊢}{x}\left({z}\right)\in \left({A}×{B}\right)\to {2}^{nd}\left({x}\left({z}\right)\right)\in {B}$
21 14 20 syl ${⊢}\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {z}\in {C}\right)\to {2}^{nd}\left({x}\left({z}\right)\right)\in {B}$
22 21 5 fmptd ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\to {R}:{C}⟶{B}$
23 2 3 elmap ${⊢}{R}\in \left({{B}}^{{C}}\right)↔{R}:{C}⟶{B}$
24 22 23 sylibr ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\to {R}\in \left({{B}}^{{C}}\right)$
25 19 24 opelxpd ${⊢}{x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\to ⟨{D},{R}⟩\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)$
26 xp1st ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {1}^{st}\left({y}\right)\in \left({{A}}^{{C}}\right)$
27 1 3 elmap ${⊢}{1}^{st}\left({y}\right)\in \left({{A}}^{{C}}\right)↔{1}^{st}\left({y}\right):{C}⟶{A}$
28 26 27 sylib ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {1}^{st}\left({y}\right):{C}⟶{A}$
29 28 ffvelrnda ${⊢}\left({y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\wedge {z}\in {C}\right)\to {1}^{st}\left({y}\right)\left({z}\right)\in {A}$
30 xp2nd ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {2}^{nd}\left({y}\right)\in \left({{B}}^{{C}}\right)$
31 2 3 elmap ${⊢}{2}^{nd}\left({y}\right)\in \left({{B}}^{{C}}\right)↔{2}^{nd}\left({y}\right):{C}⟶{B}$
32 30 31 sylib ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {2}^{nd}\left({y}\right):{C}⟶{B}$
33 32 ffvelrnda ${⊢}\left({y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\wedge {z}\in {C}\right)\to {2}^{nd}\left({y}\right)\left({z}\right)\in {B}$
34 29 33 opelxpd ${⊢}\left({y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\wedge {z}\in {C}\right)\to ⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\in \left({A}×{B}\right)$
35 34 6 fmptd ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {S}:{C}⟶{A}×{B}$
36 11 3 elmap ${⊢}{S}\in \left({\left({A}×{B}\right)}^{{C}}\right)↔{S}:{C}⟶{A}×{B}$
37 35 36 sylibr ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {S}\in \left({\left({A}×{B}\right)}^{{C}}\right)$
38 1st2nd2 ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {y}=⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩$
39 38 ad2antlr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {y}=⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩$
40 28 feqmptd ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {1}^{st}\left({y}\right)=\left({z}\in {C}⟼{1}^{st}\left({y}\right)\left({z}\right)\right)$
41 40 ad2antlr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {1}^{st}\left({y}\right)=\left({z}\in {C}⟼{1}^{st}\left({y}\right)\left({z}\right)\right)$
42 simplr ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {x}={S}$
43 42 fveq1d ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {x}\left({z}\right)={S}\left({z}\right)$
44 opex ${⊢}⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\in \mathrm{V}$
45 6 fvmpt2 ${⊢}\left({z}\in {C}\wedge ⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\in \mathrm{V}\right)\to {S}\left({z}\right)=⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩$
46 44 45 mpan2 ${⊢}{z}\in {C}\to {S}\left({z}\right)=⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩$
47 46 adantl ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {S}\left({z}\right)=⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩$
48 43 47 eqtrd ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {x}\left({z}\right)=⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩$
49 48 fveq2d ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {1}^{st}\left({x}\left({z}\right)\right)={1}^{st}\left(⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)$
50 fvex ${⊢}{1}^{st}\left({y}\right)\left({z}\right)\in \mathrm{V}$
51 fvex ${⊢}{2}^{nd}\left({y}\right)\left({z}\right)\in \mathrm{V}$
52 50 51 op1st ${⊢}{1}^{st}\left(⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)={1}^{st}\left({y}\right)\left({z}\right)$
53 49 52 syl6eq ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {1}^{st}\left({x}\left({z}\right)\right)={1}^{st}\left({y}\right)\left({z}\right)$
54 53 mpteq2dva ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to \left({z}\in {C}⟼{1}^{st}\left({x}\left({z}\right)\right)\right)=\left({z}\in {C}⟼{1}^{st}\left({y}\right)\left({z}\right)\right)$
55 4 54 syl5eq ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {D}=\left({z}\in {C}⟼{1}^{st}\left({y}\right)\left({z}\right)\right)$
56 41 55 eqtr4d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {1}^{st}\left({y}\right)={D}$
57 32 feqmptd ${⊢}{y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\to {2}^{nd}\left({y}\right)=\left({z}\in {C}⟼{2}^{nd}\left({y}\right)\left({z}\right)\right)$
58 57 ad2antlr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {2}^{nd}\left({y}\right)=\left({z}\in {C}⟼{2}^{nd}\left({y}\right)\left({z}\right)\right)$
59 48 fveq2d ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {2}^{nd}\left({x}\left({z}\right)\right)={2}^{nd}\left(⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)$
60 50 51 op2nd ${⊢}{2}^{nd}\left(⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)={2}^{nd}\left({y}\right)\left({z}\right)$
61 59 60 syl6eq ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\wedge {z}\in {C}\right)\to {2}^{nd}\left({x}\left({z}\right)\right)={2}^{nd}\left({y}\right)\left({z}\right)$
62 61 mpteq2dva ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to \left({z}\in {C}⟼{2}^{nd}\left({x}\left({z}\right)\right)\right)=\left({z}\in {C}⟼{2}^{nd}\left({y}\right)\left({z}\right)\right)$
63 5 62 syl5eq ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {R}=\left({z}\in {C}⟼{2}^{nd}\left({y}\right)\left({z}\right)\right)$
64 58 63 eqtr4d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {2}^{nd}\left({y}\right)={R}$
65 56 64 opeq12d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to ⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩=⟨{D},{R}⟩$
66 39 65 eqtrd ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {x}={S}\right)\to {y}=⟨{D},{R}⟩$
67 simpll ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {x}\in \left({\left({A}×{B}\right)}^{{C}}\right)$
68 67 12 sylib ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {x}:{C}⟶{A}×{B}$
69 68 feqmptd ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {x}=\left({z}\in {C}⟼{x}\left({z}\right)\right)$
70 simpr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {y}=⟨{D},{R}⟩$
71 70 fveq2d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {1}^{st}\left({y}\right)={1}^{st}\left(⟨{D},{R}⟩\right)$
72 19 ad2antrr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {D}\in \left({{A}}^{{C}}\right)$
73 24 ad2antrr ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {R}\in \left({{B}}^{{C}}\right)$
74 op1stg ${⊢}\left({D}\in \left({{A}}^{{C}}\right)\wedge {R}\in \left({{B}}^{{C}}\right)\right)\to {1}^{st}\left(⟨{D},{R}⟩\right)={D}$
75 72 73 74 syl2anc ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {1}^{st}\left(⟨{D},{R}⟩\right)={D}$
76 71 75 eqtrd ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {1}^{st}\left({y}\right)={D}$
77 76 fveq1d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {1}^{st}\left({y}\right)\left({z}\right)={D}\left({z}\right)$
78 fvex ${⊢}{1}^{st}\left({x}\left({z}\right)\right)\in \mathrm{V}$
79 4 fvmpt2 ${⊢}\left({z}\in {C}\wedge {1}^{st}\left({x}\left({z}\right)\right)\in \mathrm{V}\right)\to {D}\left({z}\right)={1}^{st}\left({x}\left({z}\right)\right)$
80 78 79 mpan2 ${⊢}{z}\in {C}\to {D}\left({z}\right)={1}^{st}\left({x}\left({z}\right)\right)$
81 77 80 sylan9eq ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to {1}^{st}\left({y}\right)\left({z}\right)={1}^{st}\left({x}\left({z}\right)\right)$
82 70 fveq2d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {2}^{nd}\left({y}\right)={2}^{nd}\left(⟨{D},{R}⟩\right)$
83 op2ndg ${⊢}\left({D}\in \left({{A}}^{{C}}\right)\wedge {R}\in \left({{B}}^{{C}}\right)\right)\to {2}^{nd}\left(⟨{D},{R}⟩\right)={R}$
84 72 73 83 syl2anc ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {2}^{nd}\left(⟨{D},{R}⟩\right)={R}$
85 82 84 eqtrd ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {2}^{nd}\left({y}\right)={R}$
86 85 fveq1d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {2}^{nd}\left({y}\right)\left({z}\right)={R}\left({z}\right)$
87 fvex ${⊢}{2}^{nd}\left({x}\left({z}\right)\right)\in \mathrm{V}$
88 5 fvmpt2 ${⊢}\left({z}\in {C}\wedge {2}^{nd}\left({x}\left({z}\right)\right)\in \mathrm{V}\right)\to {R}\left({z}\right)={2}^{nd}\left({x}\left({z}\right)\right)$
89 87 88 mpan2 ${⊢}{z}\in {C}\to {R}\left({z}\right)={2}^{nd}\left({x}\left({z}\right)\right)$
90 86 89 sylan9eq ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to {2}^{nd}\left({y}\right)\left({z}\right)={2}^{nd}\left({x}\left({z}\right)\right)$
91 81 90 opeq12d ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to ⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩=⟨{1}^{st}\left({x}\left({z}\right)\right),{2}^{nd}\left({x}\left({z}\right)\right)⟩$
92 68 ffvelrnda ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to {x}\left({z}\right)\in \left({A}×{B}\right)$
93 1st2nd2 ${⊢}{x}\left({z}\right)\in \left({A}×{B}\right)\to {x}\left({z}\right)=⟨{1}^{st}\left({x}\left({z}\right)\right),{2}^{nd}\left({x}\left({z}\right)\right)⟩$
94 92 93 syl ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to {x}\left({z}\right)=⟨{1}^{st}\left({x}\left({z}\right)\right),{2}^{nd}\left({x}\left({z}\right)\right)⟩$
95 91 94 eqtr4d ${⊢}\left(\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\wedge {z}\in {C}\right)\to ⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩={x}\left({z}\right)$
96 95 mpteq2dva ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to \left({z}\in {C}⟼⟨{1}^{st}\left({y}\right)\left({z}\right),{2}^{nd}\left({y}\right)\left({z}\right)⟩\right)=\left({z}\in {C}⟼{x}\left({z}\right)\right)$
97 6 96 syl5eq ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {S}=\left({z}\in {C}⟼{x}\left({z}\right)\right)$
98 69 97 eqtr4d ${⊢}\left(\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\wedge {y}=⟨{D},{R}⟩\right)\to {x}={S}$
99 66 98 impbida ${⊢}\left({x}\in \left({\left({A}×{B}\right)}^{{C}}\right)\wedge {y}\in \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)\right)\to \left({x}={S}↔{y}=⟨{D},{R}⟩\right)$
100 7 10 25 37 99 en3i ${⊢}\left({\left({A}×{B}\right)}^{{C}}\right)\approx \left(\left({{A}}^{{C}}\right)×\left({{B}}^{{C}}\right)\right)$