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 ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ≈ ( 𝐵 ↑m 𝐷 ) )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
2 bren ⊢ ( 𝐶 ≈ 𝐷 ↔ ∃ 𝑔 𝑔 : 𝐶 –1-1-onto→ 𝐷 )
3 exdistrv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑔 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) )
4 ovexd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ∈ V )
5 ovexd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝐵 ↑m 𝐷 ) ∈ V )
6 elmapi ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 𝐶 ) → 𝑥 : 𝐶 ⟶ 𝐴 )
7 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
8 7 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
9 fco ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 : 𝐶 ⟶ 𝐴 ) → ( 𝑓 ∘ 𝑥 ) : 𝐶 ⟶ 𝐵 )
10 8 9 sylan ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐶 ⟶ 𝐴 ) → ( 𝑓 ∘ 𝑥 ) : 𝐶 ⟶ 𝐵 )
11 f1ocnv ⊢ ( 𝑔 : 𝐶 –1-1-onto→ 𝐷 → ◡ 𝑔 : 𝐷 –1-1-onto→ 𝐶 )
12 11 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ◡ 𝑔 : 𝐷 –1-1-onto→ 𝐶 )
13 f1of ⊢ ( ◡ 𝑔 : 𝐷 –1-1-onto→ 𝐶 → ◡ 𝑔 : 𝐷 ⟶ 𝐶 )
14 12 13 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ◡ 𝑔 : 𝐷 ⟶ 𝐶 )
15 14 adantr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐶 ⟶ 𝐴 ) → ◡ 𝑔 : 𝐷 ⟶ 𝐶 )
16 fco ⊢ ( ( ( 𝑓 ∘ 𝑥 ) : 𝐶 ⟶ 𝐵 ∧ ◡ 𝑔 : 𝐷 ⟶ 𝐶 ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 )
17 10 15 16 syl2anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐶 ⟶ 𝐴 ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 )
18 17 ex ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 : 𝐶 ⟶ 𝐴 → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 ) )
19 6 18 syl5 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 ∈ ( 𝐴 ↑m 𝐶 ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 ) )
20 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
21 20 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝑓 : 𝐴 –onto→ 𝐵 )
22 forn ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ran 𝑓 = 𝐵 )
23 21 22 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ran 𝑓 = 𝐵 )
24 vex ⊢ 𝑓 ∈ V
25 24 rnex ⊢ ran 𝑓 ∈ V
26 23 25 eqeltrrdi ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝐵 ∈ V )
27 f1ofo ⊢ ( 𝑔 : 𝐶 –1-1-onto→ 𝐷 → 𝑔 : 𝐶 –onto→ 𝐷 )
28 27 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝑔 : 𝐶 –onto→ 𝐷 )
29 forn ⊢ ( 𝑔 : 𝐶 –onto→ 𝐷 → ran 𝑔 = 𝐷 )
30 28 29 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ran 𝑔 = 𝐷 )
31 vex ⊢ 𝑔 ∈ V
32 31 rnex ⊢ ran 𝑔 ∈ V
33 30 32 eqeltrrdi ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝐷 ∈ V )
34 26 33 elmapd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 ) )
35 19 34 sylibrd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 ∈ ( 𝐴 ↑m 𝐶 ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ ( 𝐵 ↑m 𝐷 ) ) )
36 elmapi ⊢ ( 𝑦 ∈ ( 𝐵 ↑m 𝐷 ) → 𝑦 : 𝐷 ⟶ 𝐵 )
37 f1ocnv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
38 37 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
39 f1of ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐵 ⟶ 𝐴 )
40 38 39 syl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ◡ 𝑓 : 𝐵 ⟶ 𝐴 )
41 40 adantr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) → ◡ 𝑓 : 𝐵 ⟶ 𝐴 )
42 id ⊢ ( 𝑦 : 𝐷 ⟶ 𝐵 → 𝑦 : 𝐷 ⟶ 𝐵 )
43 f1of ⊢ ( 𝑔 : 𝐶 –1-1-onto→ 𝐷 → 𝑔 : 𝐶 ⟶ 𝐷 )
44 43 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝑔 : 𝐶 ⟶ 𝐷 )
45 fco ⊢ ( ( 𝑦 : 𝐷 ⟶ 𝐵 ∧ 𝑔 : 𝐶 ⟶ 𝐷 ) → ( 𝑦 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
46 42 44 45 syl2anr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) → ( 𝑦 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
47 fco ⊢ ( ( ◡ 𝑓 : 𝐵 ⟶ 𝐴 ∧ ( 𝑦 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 ) → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 )
48 41 46 47 syl2anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 )
49 48 ex ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 : 𝐷 ⟶ 𝐵 → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 ) )
50 36 49 syl5 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 ∈ ( 𝐵 ↑m 𝐷 ) → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 ) )
51 f1odm ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → dom 𝑓 = 𝐴 )
52 51 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → dom 𝑓 = 𝐴 )
53 24 dmex ⊢ dom 𝑓 ∈ V
54 52 53 eqeltrrdi ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝐴 ∈ V )
55 f1odm ⊢ ( 𝑔 : 𝐶 –1-1-onto→ 𝐷 → dom 𝑔 = 𝐶 )
56 55 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → dom 𝑔 = 𝐶 )
57 31 dmex ⊢ dom 𝑔 ∈ V
58 56 57 eqeltrrdi ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → 𝐶 ∈ V )
59 54 58 elmapd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ ( 𝐴 ↑m 𝐶 ) ↔ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 ) )
60 50 59 sylibrd ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 ∈ ( 𝐵 ↑m 𝐷 ) → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ ( 𝐴 ↑m 𝐶 ) ) )
61 coass ⊢ ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) )
62 f1ococnv2 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ 𝐵 ) )
63 62 ad2antrr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( 𝑓 ∘ ◡ 𝑓 ) = ( I ↾ 𝐵 ) )
64 63 coeq1d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( ( I ↾ 𝐵 ) ∘ ( 𝑦 ∘ 𝑔 ) ) )
65 46 adantrl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( 𝑦 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 )
66 fcoi2 ⊢ ( ( 𝑦 ∘ 𝑔 ) : 𝐶 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
67 65 66 syl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
68 64 67 eqtrd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ ◡ 𝑓 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
69 61 68 syl5eqr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) = ( 𝑦 ∘ 𝑔 ) )
70 69 eqeq2d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( 𝑓 ∘ 𝑥 ) = ( 𝑦 ∘ 𝑔 ) ) )
71 coass ⊢ ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( ( 𝑓 ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) )
72 f1ococnv1 ⊢ ( 𝑔 : 𝐶 –1-1-onto→ 𝐷 → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐶 ) )
73 72 ad2antlr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐶 ) )
74 73 coeq2d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( ( 𝑓 ∘ 𝑥 ) ∘ ( I ↾ 𝐶 ) ) )
75 10 adantrr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( 𝑓 ∘ 𝑥 ) : 𝐶 ⟶ 𝐵 )
76 fcoi1 ⊢ ( ( 𝑓 ∘ 𝑥 ) : 𝐶 ⟶ 𝐵 → ( ( 𝑓 ∘ 𝑥 ) ∘ ( I ↾ 𝐶 ) ) = ( 𝑓 ∘ 𝑥 ) )
77 75 76 syl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ( I ↾ 𝐶 ) ) = ( 𝑓 ∘ 𝑥 ) )
78 74 77 eqtrd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( 𝑓 ∘ 𝑥 ) )
79 71 78 syl5eq ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( 𝑓 ∘ 𝑥 ) )
80 79 eqeq2d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ ( 𝑦 ∘ 𝑔 ) = ( 𝑓 ∘ 𝑥 ) ) )
81 eqcom ⊢ ( ( 𝑦 ∘ 𝑔 ) = ( 𝑓 ∘ 𝑥 ) ↔ ( 𝑓 ∘ 𝑥 ) = ( 𝑦 ∘ 𝑔 ) )
82 80 81 syl6bb ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ ( 𝑓 ∘ 𝑥 ) = ( 𝑦 ∘ 𝑔 ) ) )
83 70 82 bitr4d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( 𝑦 ∘ 𝑔 ) = ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ) )
84 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –1-1→ 𝐵 )
85 84 ad2antrr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
86 simprl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → 𝑥 : 𝐶 ⟶ 𝐴 )
87 48 adantrl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 )
88 cocan1 ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 : 𝐶 ⟶ 𝐴 ∧ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐶 ⟶ 𝐴 ) → ( ( 𝑓 ∘ 𝑥 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
89 85 86 87 88 syl3anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) = ( 𝑓 ∘ ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
90 28 adantr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → 𝑔 : 𝐶 –onto→ 𝐷 )
91 ffn ⊢ ( 𝑦 : 𝐷 ⟶ 𝐵 → 𝑦 Fn 𝐷 )
92 91 ad2antll ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → 𝑦 Fn 𝐷 )
93 17 adantrr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐷 ⟶ 𝐵 )
94 93 ffnd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐷 )
95 cocan2 ⊢ ( ( 𝑔 : 𝐶 –onto→ 𝐷 ∧ 𝑦 Fn 𝐷 ∧ ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐷 ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
96 90 92 94 95 syl3anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
97 83 89 96 3bitr3d ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) ) → ( 𝑥 = ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
98 97 ex ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 : 𝐶 ⟶ 𝐴 ∧ 𝑦 : 𝐷 ⟶ 𝐵 ) → ( 𝑥 = ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
99 6 36 98 syl2ani ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 ∈ ( 𝐴 ↑m 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ↑m 𝐷 ) ) → ( 𝑥 = ( ◡ 𝑓 ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( 𝑓 ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
100 4 5 35 60 99 en3d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ≈ ( 𝐵 ↑m 𝐷 ) )
101 100 exlimivv ⊢ ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ≈ ( 𝐵 ↑m 𝐷 ) )
102 3 101 sylbir ⊢ ( ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑔 𝑔 : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ≈ ( 𝐵 ↑m 𝐷 ) )
103 1 2 102 syl2anb ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → ( 𝐴 ↑m 𝐶 ) ≈ ( 𝐵 ↑m 𝐷 ) )