This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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