# Metamath Proof Explorer

## Theorem mapen

Description: Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of Enderton p. 139. (Contributed by NM, 16-Dec-2003) (Proof shortened by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion mapen ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({{A}}^{{C}}\right)\approx \left({{B}}^{{D}}\right)$

### Proof

Step Hyp Ref Expression
1 bren ${⊢}{A}\approx {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}$
2 bren ${⊢}{C}\approx {D}↔\exists {g}\phantom{\rule{.4em}{0ex}}{g}:{C}\underset{1-1 onto}{⟶}{D}$
3 exdistrv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\wedge \exists {g}\phantom{\rule{.4em}{0ex}}{g}:{C}\underset{1-1 onto}{⟶}{D}\right)$
4 ovexd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{A}}^{{C}}\in \mathrm{V}$
5 ovexd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{B}}^{{D}}\in \mathrm{V}$
6 elmapi ${⊢}{x}\in \left({{A}}^{{C}}\right)\to {x}:{C}⟶{A}$
7 f1of ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}⟶{B}$
8 7 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {f}:{A}⟶{B}$
9 fco ${⊢}\left({f}:{A}⟶{B}\wedge {x}:{C}⟶{A}\right)\to \left({f}\circ {x}\right):{C}⟶{B}$
10 8 9 sylan ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {x}:{C}⟶{A}\right)\to \left({f}\circ {x}\right):{C}⟶{B}$
11 f1ocnv ${⊢}{g}:{C}\underset{1-1 onto}{⟶}{D}\to {{g}}^{-1}:{D}\underset{1-1 onto}{⟶}{C}$
12 11 adantl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{g}}^{-1}:{D}\underset{1-1 onto}{⟶}{C}$
13 f1of ${⊢}{{g}}^{-1}:{D}\underset{1-1 onto}{⟶}{C}\to {{g}}^{-1}:{D}⟶{C}$
14 12 13 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{g}}^{-1}:{D}⟶{C}$
15 14 adantr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {x}:{C}⟶{A}\right)\to {{g}}^{-1}:{D}⟶{C}$
16 fco ${⊢}\left(\left({f}\circ {x}\right):{C}⟶{B}\wedge {{g}}^{-1}:{D}⟶{C}\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}$
17 10 15 16 syl2anc ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {x}:{C}⟶{A}\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}$
18 17 ex ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({x}:{C}⟶{A}\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}\right)$
19 6 18 syl5 ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({x}\in \left({{A}}^{{C}}\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}\right)$
20 f1ofo ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}\underset{onto}{⟶}{B}$
21 20 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {f}:{A}\underset{onto}{⟶}{B}$
22 forn ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
23 21 22 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \mathrm{ran}{f}={B}$
24 vex ${⊢}{f}\in \mathrm{V}$
25 24 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
26 23 25 eqeltrrdi ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {B}\in \mathrm{V}$
27 f1ofo ${⊢}{g}:{C}\underset{1-1 onto}{⟶}{D}\to {g}:{C}\underset{onto}{⟶}{D}$
28 27 adantl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {g}:{C}\underset{onto}{⟶}{D}$
29 forn ${⊢}{g}:{C}\underset{onto}{⟶}{D}\to \mathrm{ran}{g}={D}$
30 28 29 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \mathrm{ran}{g}={D}$
31 vex ${⊢}{g}\in \mathrm{V}$
32 31 rnex ${⊢}\mathrm{ran}{g}\in \mathrm{V}$
33 30 32 eqeltrrdi ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {D}\in \mathrm{V}$
34 26 33 elmapd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\in \left({{B}}^{{D}}\right)↔\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}\right)$
35 19 34 sylibrd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({x}\in \left({{A}}^{{C}}\right)\to \left({f}\circ {x}\right)\circ {{g}}^{-1}\in \left({{B}}^{{D}}\right)\right)$
36 elmapi ${⊢}{y}\in \left({{B}}^{{D}}\right)\to {y}:{D}⟶{B}$
37 f1ocnv ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
38 37 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
39 f1of ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}:{B}⟶{A}$
40 38 39 syl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {{f}}^{-1}:{B}⟶{A}$
41 40 adantr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {y}:{D}⟶{B}\right)\to {{f}}^{-1}:{B}⟶{A}$
42 id ${⊢}{y}:{D}⟶{B}\to {y}:{D}⟶{B}$
43 f1of ${⊢}{g}:{C}\underset{1-1 onto}{⟶}{D}\to {g}:{C}⟶{D}$
44 43 adantl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {g}:{C}⟶{D}$
45 fco ${⊢}\left({y}:{D}⟶{B}\wedge {g}:{C}⟶{D}\right)\to \left({y}\circ {g}\right):{C}⟶{B}$
46 42 44 45 syl2anr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {y}:{D}⟶{B}\right)\to \left({y}\circ {g}\right):{C}⟶{B}$
47 fco ${⊢}\left({{f}}^{-1}:{B}⟶{A}\wedge \left({y}\circ {g}\right):{C}⟶{B}\right)\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}$
48 41 46 47 syl2anc ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge {y}:{D}⟶{B}\right)\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}$
49 48 ex ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({y}:{D}⟶{B}\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}\right)$
50 36 49 syl5 ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({y}\in \left({{B}}^{{D}}\right)\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}\right)$
51 f1odm ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{dom}{f}={A}$
52 51 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \mathrm{dom}{f}={A}$
53 24 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
54 52 53 eqeltrrdi ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {A}\in \mathrm{V}$
55 f1odm ${⊢}{g}:{C}\underset{1-1 onto}{⟶}{D}\to \mathrm{dom}{g}={C}$
56 55 adantl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \mathrm{dom}{g}={C}$
57 31 dmex ${⊢}\mathrm{dom}{g}\in \mathrm{V}$
58 56 57 eqeltrrdi ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to {C}\in \mathrm{V}$
59 54 58 elmapd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\in \left({{A}}^{{C}}\right)↔\left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}\right)$
60 50 59 sylibrd ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({y}\in \left({{B}}^{{D}}\right)\to {{f}}^{-1}\circ \left({y}\circ {g}\right)\in \left({{A}}^{{C}}\right)\right)$
61 coass ${⊢}\left({f}\circ {{f}}^{-1}\right)\circ \left({y}\circ {g}\right)={f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)$
62 f1ococnv2 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}\circ {{f}}^{-1}={\mathrm{I}↾}_{{B}}$
63 62 ad2antrr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {f}\circ {{f}}^{-1}={\mathrm{I}↾}_{{B}}$
64 63 coeq1d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {{f}}^{-1}\right)\circ \left({y}\circ {g}\right)=\left({\mathrm{I}↾}_{{B}}\right)\circ \left({y}\circ {g}\right)$
65 46 adantrl ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({y}\circ {g}\right):{C}⟶{B}$
66 fcoi2 ${⊢}\left({y}\circ {g}\right):{C}⟶{B}\to \left({\mathrm{I}↾}_{{B}}\right)\circ \left({y}\circ {g}\right)={y}\circ {g}$
67 65 66 syl ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({\mathrm{I}↾}_{{B}}\right)\circ \left({y}\circ {g}\right)={y}\circ {g}$
68 64 67 eqtrd ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {{f}}^{-1}\right)\circ \left({y}\circ {g}\right)={y}\circ {g}$
69 61 68 syl5eqr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)={y}\circ {g}$
70 69 eqeq2d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}={f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)↔{f}\circ {x}={y}\circ {g}\right)$
71 coass ${⊢}\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}=\left({f}\circ {x}\right)\circ \left({{g}}^{-1}\circ {g}\right)$
72 f1ococnv1 ${⊢}{g}:{C}\underset{1-1 onto}{⟶}{D}\to {{g}}^{-1}\circ {g}={\mathrm{I}↾}_{{C}}$
73 72 ad2antlr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {{g}}^{-1}\circ {g}={\mathrm{I}↾}_{{C}}$
74 73 coeq2d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}\right)\circ \left({{g}}^{-1}\circ {g}\right)=\left({f}\circ {x}\right)\circ \left({\mathrm{I}↾}_{{C}}\right)$
75 10 adantrr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}\right):{C}⟶{B}$
76 fcoi1 ${⊢}\left({f}\circ {x}\right):{C}⟶{B}\to \left({f}\circ {x}\right)\circ \left({\mathrm{I}↾}_{{C}}\right)={f}\circ {x}$
77 75 76 syl ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}\right)\circ \left({\mathrm{I}↾}_{{C}}\right)={f}\circ {x}$
78 74 77 eqtrd ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}\right)\circ \left({{g}}^{-1}\circ {g}\right)={f}\circ {x}$
79 71 78 syl5eq ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}={f}\circ {x}$
80 79 eqeq2d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({y}\circ {g}=\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}↔{y}\circ {g}={f}\circ {x}\right)$
81 eqcom ${⊢}{y}\circ {g}={f}\circ {x}↔{f}\circ {x}={y}\circ {g}$
82 80 81 syl6bb ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({y}\circ {g}=\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}↔{f}\circ {x}={y}\circ {g}\right)$
83 70 82 bitr4d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}={f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)↔{y}\circ {g}=\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}\right)$
84 f1of1 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}\underset{1-1}{⟶}{B}$
85 84 ad2antrr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {f}:{A}\underset{1-1}{⟶}{B}$
86 simprl ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {x}:{C}⟶{A}$
87 48 adantrl ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}$
88 cocan1 ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {x}:{C}⟶{A}\wedge \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right):{C}⟶{A}\right)\to \left({f}\circ {x}={f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)↔{x}={{f}}^{-1}\circ \left({y}\circ {g}\right)\right)$
89 85 86 87 88 syl3anc ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({f}\circ {x}={f}\circ \left({{f}}^{-1}\circ \left({y}\circ {g}\right)\right)↔{x}={{f}}^{-1}\circ \left({y}\circ {g}\right)\right)$
90 28 adantr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {g}:{C}\underset{onto}{⟶}{D}$
91 ffn ${⊢}{y}:{D}⟶{B}\to {y}Fn{D}$
92 91 ad2antll ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to {y}Fn{D}$
93 17 adantrr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right):{D}⟶{B}$
94 93 ffnd ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)Fn{D}$
95 cocan2 ${⊢}\left({g}:{C}\underset{onto}{⟶}{D}\wedge {y}Fn{D}\wedge \left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)Fn{D}\right)\to \left({y}\circ {g}=\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}↔{y}=\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)$
96 90 92 94 95 syl3anc ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({y}\circ {g}=\left(\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\circ {g}↔{y}=\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)$
97 83 89 96 3bitr3d ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\wedge \left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\right)\to \left({x}={{f}}^{-1}\circ \left({y}\circ {g}\right)↔{y}=\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)$
98 97 ex ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left(\left({x}:{C}⟶{A}\wedge {y}:{D}⟶{B}\right)\to \left({x}={{f}}^{-1}\circ \left({y}\circ {g}\right)↔{y}=\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\right)$
99 6 36 98 syl2ani ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left(\left({x}\in \left({{A}}^{{C}}\right)\wedge {y}\in \left({{B}}^{{D}}\right)\right)\to \left({x}={{f}}^{-1}\circ \left({y}\circ {g}\right)↔{y}=\left({f}\circ {x}\right)\circ {{g}}^{-1}\right)\right)$
100 4 5 35 60 99 en3d ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({{A}}^{{C}}\right)\approx \left({{B}}^{{D}}\right)$
101 100 exlimivv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({{A}}^{{C}}\right)\approx \left({{B}}^{{D}}\right)$
102 3 101 sylbir ${⊢}\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\wedge \exists {g}\phantom{\rule{.4em}{0ex}}{g}:{C}\underset{1-1 onto}{⟶}{D}\right)\to \left({{A}}^{{C}}\right)\approx \left({{B}}^{{D}}\right)$
103 1 2 102 syl2anb ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({{A}}^{{C}}\right)\approx \left({{B}}^{{D}}\right)$