Metamath Proof Explorer

Theorem hashfacen

Description: The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015)

Ref Expression
Assertion hashfacen ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )

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 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 → 𝑓 : 𝐴 ⟶ 𝐶 )
5 f1odm ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → dom ℎ = 𝐶 )
6 vex ⊢ ℎ ∈ V
7 6 dmex ⊢ dom ℎ ∈ V
8 5 7 syl6eqelr ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → 𝐶 ∈ V )
9 f1odm ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → dom 𝑔 = 𝐴 )
10 vex ⊢ 𝑔 ∈ V
11 10 dmex ⊢ dom 𝑔 ∈ V
12 9 11 syl6eqelr ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → 𝐴 ∈ V )
13 elmapg ⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
14 8 12 13 syl2anr ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
15 4 14 syl5ibr ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 → 𝑓 ∈ ( 𝐶 ↑m 𝐴 ) ) )
16 15 abssdv ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ⊆ ( 𝐶 ↑m 𝐴 ) )
17 ovex ⊢ ( 𝐶 ↑m 𝐴 ) ∈ V
18 17 ssex ⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ⊆ ( 𝐶 ↑m 𝐴 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∈ V )
19 16 18 syl ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∈ V )
20 f1of ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 → 𝑓 : 𝐵 ⟶ 𝐷 )
21 f1ofo ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ℎ : 𝐶 –onto→ 𝐷 )
22 forn ⊢ ( ℎ : 𝐶 –onto→ 𝐷 → ran ℎ = 𝐷 )
23 21 22 syl ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ran ℎ = 𝐷 )
24 6 rnex ⊢ ran ℎ ∈ V
25 23 24 syl6eqelr ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → 𝐷 ∈ V )
26 f1ofo ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → 𝑔 : 𝐴 –onto→ 𝐵 )
27 forn ⊢ ( 𝑔 : 𝐴 –onto→ 𝐵 → ran 𝑔 = 𝐵 )
28 26 27 syl ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ran 𝑔 = 𝐵 )
29 10 rnex ⊢ ran 𝑔 ∈ V
30 28 29 syl6eqelr ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ V )
31 elmapg ⊢ ( ( 𝐷 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑓 ∈ ( 𝐷 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝐷 ) )
32 25 30 31 syl2anr ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑓 ∈ ( 𝐷 ↑m 𝐵 ) ↔ 𝑓 : 𝐵 ⟶ 𝐷 ) )
33 20 32 syl5ibr ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 → 𝑓 ∈ ( 𝐷 ↑m 𝐵 ) ) )
34 33 abssdv ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ⊆ ( 𝐷 ↑m 𝐵 ) )
35 ovex ⊢ ( 𝐷 ↑m 𝐵 ) ∈ V
36 35 ssex ⊢ ( { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ⊆ ( 𝐷 ↑m 𝐵 ) → { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ∈ V )
37 34 36 syl ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ∈ V )
38 f1oco ⊢ ( ( ℎ : 𝐶 –1-1-onto→ 𝐷 ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
39 38 adantll ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
40 f1ocnv ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
41 40 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
42 f1oco ⊢ ( ( ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 ∧ ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
43 39 41 42 syl2anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
44 43 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 ) )
45 vex ⊢ 𝑥 ∈ V
46 f1oeq1 ⊢ ( 𝑓 = 𝑥 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) )
47 45 46 elab ⊢ ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐶 )
48 6 45 coex ⊢ ( ℎ ∘ 𝑥 ) ∈ V
49 10 cnvex ⊢ ◡ 𝑔 ∈ V
50 48 49 coex ⊢ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ V
51 f1oeq1 ⊢ ( 𝑓 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) → ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 ↔ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 ) )
52 50 51 elab ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ↔ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
53 44 47 52 3imtr4g ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) )
54 f1ocnv ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 )
55 54 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 )
56 f1oco ⊢ ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
57 56 ancoms ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
58 57 adantlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
59 f1oco ⊢ ( ( ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 ∧ ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
60 55 58 59 syl2anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
61 60 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 ) )
62 vex ⊢ 𝑦 ∈ V
63 f1oeq1 ⊢ ( 𝑓 = 𝑦 → ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 ↔ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) )
64 62 63 elab ⊢ ( 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ↔ 𝑦 : 𝐵 –1-1-onto→ 𝐷 )
65 6 cnvex ⊢ ◡ ℎ ∈ V
66 62 10 coex ⊢ ( 𝑦 ∘ 𝑔 ) ∈ V
67 65 66 coex ⊢ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ V
68 f1oeq1 ⊢ ( 𝑓 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 ↔ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 ) )
69 67 68 elab ⊢ ( ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ↔ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
70 61 64 69 3imtr4g ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ) )
71 47 64 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∧ 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) ↔ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) )
72 coass ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) )
73 f1ococnv1 ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐴 ) )
74 73 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐴 ) )
75 74 coeq2d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) )
76 39 adantrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
77 f1of ⊢ ( ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 → ( ℎ ∘ 𝑥 ) : 𝐴 ⟶ 𝐷 )
78 fcoi1 ⊢ ( ( ℎ ∘ 𝑥 ) : 𝐴 ⟶ 𝐷 → ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) = ( ℎ ∘ 𝑥 ) )
79 76 77 78 3syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) = ( ℎ ∘ 𝑥 ) )
80 75 79 eqtrd ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( ℎ ∘ 𝑥 ) )
81 72 80 syl5req ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ 𝑥 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) )
82 coass ⊢ ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) )
83 f1ococnv2 ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ( ℎ ∘ ◡ ℎ ) = ( I ↾ 𝐷 ) )
84 83 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ ◡ ℎ ) = ( I ↾ 𝐷 ) )
85 84 coeq1d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) )
86 58 adantrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
87 f1of ⊢ ( ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 → ( 𝑦 ∘ 𝑔 ) : 𝐴 ⟶ 𝐷 )
88 fcoi2 ⊢ ( ( 𝑦 ∘ 𝑔 ) : 𝐴 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
89 86 87 88 3syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
90 85 89 eqtrd ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
91 82 90 syl5eqr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) = ( 𝑦 ∘ 𝑔 ) )
92 81 91 eqeq12d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( 𝑦 ∘ 𝑔 ) ) )
93 eqcom ⊢ ( ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( 𝑦 ∘ 𝑔 ) ↔ ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) )
94 92 93 syl6bb ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ) )
95 f1of1 ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ℎ : 𝐶 –1-1→ 𝐷 )
96 95 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ℎ : 𝐶 –1-1→ 𝐷 )
97 f1of ⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 → 𝑥 : 𝐴 ⟶ 𝐶 )
98 97 ad2antrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑥 : 𝐴 ⟶ 𝐶 )
99 60 adantrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
100 f1of ⊢ ( ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 )
101 99 100 syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 )
102 cocan1 ⊢ ( ( ℎ : 𝐶 –1-1→ 𝐷 ∧ 𝑥 : 𝐴 ⟶ 𝐶 ∧ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
103 96 98 101 102 syl3anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
104 26 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑔 : 𝐴 –onto→ 𝐵 )
105 f1ofn ⊢ ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 → 𝑦 Fn 𝐵 )
106 105 ad2antll ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑦 Fn 𝐵 )
107 43 adantrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
108 f1ofn ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 )
109 107 108 syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 )
110 cocan2 ⊢ ( ( 𝑔 : 𝐴 –onto→ 𝐵 ∧ 𝑦 Fn 𝐵 ∧ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
111 104 106 109 110 syl3anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
112 94 103 111 3bitr3d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
113 112 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
114 71 113 syl5bi ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∧ 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
115 19 37 53 70 114 en3d ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
116 115 exlimivv ⊢ ( ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
117 3 116 sylbir ⊢ ( ( ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ ℎ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
118 1 2 117 syl2anb ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )