# Metamath Proof Explorer

## Theorem mapxpen

Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of TakeutiZaring p. 96. (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion mapxpen ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\approx \left({{A}}^{\left({B}×{C}\right)}\right)$

### Proof

Step Hyp Ref Expression
1 ovexd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {\left({{A}}^{{B}}\right)}^{{C}}\in \mathrm{V}$
2 ovexd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {{A}}^{\left({B}×{C}\right)}\in \mathrm{V}$
3 elmapi ${⊢}{f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\to {f}:{C}⟶{{A}}^{{B}}$
4 3 ffvelrnda ${⊢}\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {y}\in {C}\right)\to {f}\left({y}\right)\in \left({{A}}^{{B}}\right)$
5 elmapi ${⊢}{f}\left({y}\right)\in \left({{A}}^{{B}}\right)\to {f}\left({y}\right):{B}⟶{A}$
6 4 5 syl ${⊢}\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {y}\in {C}\right)\to {f}\left({y}\right):{B}⟶{A}$
7 6 ffvelrnda ${⊢}\left(\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {y}\in {C}\right)\wedge {x}\in {B}\right)\to {f}\left({y}\right)\left({x}\right)\in {A}$
8 7 an32s ${⊢}\left(\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {x}\in {B}\right)\wedge {y}\in {C}\right)\to {f}\left({y}\right)\left({x}\right)\in {A}$
9 8 ralrimiva ${⊢}\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {x}\in {B}\right)\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)\in {A}$
10 9 ralrimiva ${⊢}{f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)\in {A}$
11 eqid ${⊢}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)$
12 11 fmpo ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)\in {A}↔\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right):{B}×{C}⟶{A}$
13 10 12 sylib ${⊢}{f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\to \left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right):{B}×{C}⟶{A}$
14 simp1 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {A}\in {V}$
15 xpexg ${⊢}\left({B}\in {W}\wedge {C}\in {X}\right)\to {B}×{C}\in \mathrm{V}$
16 15 3adant1 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {B}×{C}\in \mathrm{V}$
17 elmapg ${⊢}\left({A}\in {V}\wedge {B}×{C}\in \mathrm{V}\right)\to \left(\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\in \left({{A}}^{\left({B}×{C}\right)}\right)↔\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right):{B}×{C}⟶{A}\right)$
18 14 16 17 syl2anc ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left(\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\in \left({{A}}^{\left({B}×{C}\right)}\right)↔\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right):{B}×{C}⟶{A}\right)$
19 13 18 syl5ibr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\to \left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)$
20 elmapi ${⊢}{g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\to {g}:{B}×{C}⟶{A}$
21 20 adantl ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\to {g}:{B}×{C}⟶{A}$
22 fovrn ${⊢}\left({g}:{B}×{C}⟶{A}\wedge {x}\in {B}\wedge {y}\in {C}\right)\to {x}{g}{y}\in {A}$
23 22 3expa ${⊢}\left(\left({g}:{B}×{C}⟶{A}\wedge {x}\in {B}\right)\wedge {y}\in {C}\right)\to {x}{g}{y}\in {A}$
24 23 an32s ${⊢}\left(\left({g}:{B}×{C}⟶{A}\wedge {y}\in {C}\right)\wedge {x}\in {B}\right)\to {x}{g}{y}\in {A}$
25 21 24 sylanl1 ${⊢}\left(\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\wedge {y}\in {C}\right)\wedge {x}\in {B}\right)\to {x}{g}{y}\in {A}$
26 25 fmpttd ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}$
27 elmapg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({x}\in {B}⟼{x}{g}{y}\right)\in \left({{A}}^{{B}}\right)↔\left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}\right)$
28 27 3adant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left(\left({x}\in {B}⟼{x}{g}{y}\right)\in \left({{A}}^{{B}}\right)↔\left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}\right)$
29 28 ad2antrr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\wedge {y}\in {C}\right)\to \left(\left({x}\in {B}⟼{x}{g}{y}\right)\in \left({{A}}^{{B}}\right)↔\left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}\right)$
30 26 29 mpbird ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)\in \left({{A}}^{{B}}\right)$
31 30 fmpttd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right):{C}⟶{{A}}^{{B}}$
32 31 ex ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left({g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right):{C}⟶{{A}}^{{B}}\right)$
33 ovex ${⊢}{{A}}^{{B}}\in \mathrm{V}$
34 simp3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {C}\in {X}$
35 elmapg ${⊢}\left({{A}}^{{B}}\in \mathrm{V}\wedge {C}\in {X}\right)\to \left(\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)↔\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right):{C}⟶{{A}}^{{B}}\right)$
36 33 34 35 sylancr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left(\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)↔\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right):{C}⟶{{A}}^{{B}}\right)$
37 32 36 sylibrd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left({g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\right)$
38 elmapfn ${⊢}{g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\to {g}Fn\left({B}×{C}\right)$
39 38 ad2antll ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {g}Fn\left({B}×{C}\right)$
40 fnov ${⊢}{g}Fn\left({B}×{C}\right)↔{g}=\left({x}\in {B},{y}\in {C}⟼{x}{g}{y}\right)$
41 39 40 sylib ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {g}=\left({x}\in {B},{y}\in {C}⟼{x}{g}{y}\right)$
42 simp3 ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to {y}\in {C}$
43 26 adantlrl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}$
44 43 3adant2 ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}$
45 simp1l2 ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to {B}\in {W}$
46 simp1l1 ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to {A}\in {V}$
47 fex2 ${⊢}\left(\left({x}\in {B}⟼{x}{g}{y}\right):{B}⟶{A}\wedge {B}\in {W}\wedge {A}\in {V}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)\in \mathrm{V}$
48 44 45 46 47 syl3anc ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)\in \mathrm{V}$
49 eqid ${⊢}\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)$
50 49 fvmpt2 ${⊢}\left({y}\in {C}\wedge \left({x}\in {B}⟼{x}{g}{y}\right)\in \mathrm{V}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)=\left({x}\in {B}⟼{x}{g}{y}\right)$
51 42 48 50 syl2anc ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)=\left({x}\in {B}⟼{x}{g}{y}\right)$
52 51 fveq1d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)=\left({x}\in {B}⟼{x}{g}{y}\right)\left({x}\right)$
53 simp2 ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to {x}\in {B}$
54 ovex ${⊢}{x}{g}{y}\in \mathrm{V}$
55 eqid ${⊢}\left({x}\in {B}⟼{x}{g}{y}\right)=\left({x}\in {B}⟼{x}{g}{y}\right)$
56 55 fvmpt2 ${⊢}\left({x}\in {B}\wedge {x}{g}{y}\in \mathrm{V}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)\left({x}\right)={x}{g}{y}$
57 53 54 56 sylancl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)\left({x}\right)={x}{g}{y}$
58 52 57 eqtrd ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {x}\in {B}\wedge {y}\in {C}\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)={x}{g}{y}$
59 58 mpoeq3dva ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to \left({x}\in {B},{y}\in {C}⟼\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)=\left({x}\in {B},{y}\in {C}⟼{x}{g}{y}\right)$
60 41 59 eqtr4d ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {g}=\left({x}\in {B},{y}\in {C}⟼\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
61 eqid ${⊢}{B}={B}$
62 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
63 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{x}{g}{y}\right)$
64 62 63 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)$
65 64 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)$
66 nfmpt1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)$
67 66 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)$
68 fveq1 ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to {f}\left({y}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)$
69 68 fveq1d ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to {f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)$
70 69 a1d ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \left({y}\in {C}\to {f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
71 67 70 ralrimi ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)$
72 eqid ${⊢}{C}={C}$
73 71 72 jctil ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \left({C}={C}\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
74 73 a1d ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \left({x}\in {B}\to \left({C}={C}\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)\right)$
75 65 74 ralrimi ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}={C}\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
76 mpoeq123 ${⊢}\left({B}={B}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}={C}\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\left({x}\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)\right)\to \left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)=\left({x}\in {B},{y}\in {C}⟼\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
77 61 75 76 sylancr ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)=\left({x}\in {B},{y}\in {C}⟼\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)$
78 77 eqeq2d ${⊢}{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to \left({g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)↔{g}=\left({x}\in {B},{y}\in {C}⟼\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\left({y}\right)\left({x}\right)\right)\right)$
79 60 78 syl5ibrcom ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to \left({f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\to {g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
80 3 ad2antrl ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {f}:{C}⟶{{A}}^{{B}}$
81 80 feqmptd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {f}=\left({y}\in {C}⟼{f}\left({y}\right)\right)$
82 simprl ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)$
83 82 6 sylan ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {y}\in {C}\right)\to {f}\left({y}\right):{B}⟶{A}$
84 83 feqmptd ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\wedge {y}\in {C}\right)\to {f}\left({y}\right)=\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)$
85 84 mpteq2dva ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to \left({y}\in {C}⟼{f}\left({y}\right)\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
86 81 85 eqtrd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to {f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
87 nfmpo2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)$
88 87 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)$
89 eqidd ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to {B}={B}$
90 nfmpo1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)$
91 90 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)$
92 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {C}$
93 fvex ${⊢}{f}\left({y}\right)\left({x}\right)\in \mathrm{V}$
94 11 ovmpt4g ${⊢}\left({x}\in {B}\wedge {y}\in {C}\wedge {f}\left({y}\right)\left({x}\right)\in \mathrm{V}\right)\to {x}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right){y}={f}\left({y}\right)\left({x}\right)$
95 93 94 mp3an3 ${⊢}\left({x}\in {B}\wedge {y}\in {C}\right)\to {x}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right){y}={f}\left({y}\right)\left({x}\right)$
96 oveq ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to {x}{g}{y}={x}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right){y}$
97 96 eqeq1d ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({x}{g}{y}={f}\left({y}\right)\left({x}\right)↔{x}\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right){y}={f}\left({y}\right)\left({x}\right)\right)$
98 95 97 syl5ibr ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left(\left({x}\in {B}\wedge {y}\in {C}\right)\to {x}{g}{y}={f}\left({y}\right)\left({x}\right)\right)$
99 98 expcomd ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({y}\in {C}\to \left({x}\in {B}\to {x}{g}{y}={f}\left({y}\right)\left({x}\right)\right)\right)$
100 91 92 99 ralrimd ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({y}\in {C}\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={f}\left({y}\right)\left({x}\right)\right)$
101 mpteq12 ${⊢}\left({B}={B}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{x}{g}{y}={f}\left({y}\right)\left({x}\right)\right)\to \left({x}\in {B}⟼{x}{g}{y}\right)=\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)$
102 89 100 101 syl6an ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({y}\in {C}\to \left({x}\in {B}⟼{x}{g}{y}\right)=\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
103 88 102 ralrimi ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{x}{g}{y}\right)=\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)$
104 mpteq12 ${⊢}\left({C}={C}\wedge \forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}⟼{x}{g}{y}\right)=\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
105 72 103 104 sylancr ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)=\left({y}\in {C}⟼\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
106 105 eqeq2d ${⊢}{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to \left({f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)↔{f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{f}\left({y}\right)\left({x}\right)\right)\right)\right)$
107 86 106 syl5ibrcom ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to \left({g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\to {f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)\right)$
108 79 107 impbid ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge \left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\right)\to \left({f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)↔{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\right)$
109 108 ex ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left(\left({f}\in \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\wedge {g}\in \left({{A}}^{\left({B}×{C}\right)}\right)\right)\to \left({f}=\left({y}\in {C}⟼\left({x}\in {B}⟼{x}{g}{y}\right)\right)↔{g}=\left({x}\in {B},{y}\in {C}⟼{f}\left({y}\right)\left({x}\right)\right)\right)\right)$
110 1 2 19 37 109 en3d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to \left({\left({{A}}^{{B}}\right)}^{{C}}\right)\approx \left({{A}}^{\left({B}×{C}\right)}\right)$