Metamath Proof Explorer

Theorem hashfacen

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

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 f1osetex ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∈ V
5 4 a1i ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∈ V )
6 f1osetex ⊢ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ∈ V
7 6 a1i ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ∈ V )
8 f1oco ⊢ ( ( ℎ : 𝐶 –1-1-onto→ 𝐷 ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
9 8 adantll ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
10 f1ocnv ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
11 10 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
12 f1oco ⊢ ( ( ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 ∧ ◡ 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
13 9 11 12 syl2anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
14 13 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 ) )
15 vex ⊢ 𝑥 ∈ V
16 f1oeq1 ⊢ ( 𝑓 = 𝑥 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐶 ) )
17 15 16 elab ⊢ ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐶 )
18 vex ⊢ ℎ ∈ V
19 18 15 coex ⊢ ( ℎ ∘ 𝑥 ) ∈ V
20 vex ⊢ 𝑔 ∈ V
21 20 cnvex ⊢ ◡ 𝑔 ∈ V
22 19 21 coex ⊢ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ V
23 f1oeq1 ⊢ ( 𝑓 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) → ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 ↔ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 ) )
24 22 23 elab ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ↔ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
25 14 17 24 3imtr4g ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) )
26 f1ocnv ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 )
27 26 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 )
28 f1oco ⊢ ( ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 ∧ 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
29 28 ancoms ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
30 29 adantlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
31 f1oco ⊢ ( ( ◡ ℎ : 𝐷 –1-1-onto→ 𝐶 ∧ ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
32 27 30 31 syl2anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
33 32 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 ) )
34 vex ⊢ 𝑦 ∈ V
35 f1oeq1 ⊢ ( 𝑓 = 𝑦 → ( 𝑓 : 𝐵 –1-1-onto→ 𝐷 ↔ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) )
36 34 35 elab ⊢ ( 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ↔ 𝑦 : 𝐵 –1-1-onto→ 𝐷 )
37 18 cnvex ⊢ ◡ ℎ ∈ V
38 34 20 coex ⊢ ( 𝑦 ∘ 𝑔 ) ∈ V
39 37 38 coex ⊢ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ V
40 f1oeq1 ⊢ ( 𝑓 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) → ( 𝑓 : 𝐴 –1-1-onto→ 𝐶 ↔ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 ) )
41 39 40 elab ⊢ ( ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ↔ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
42 33 36 41 3imtr4g ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ) )
43 17 36 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∧ 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) ↔ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) )
44 coass ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) )
45 f1ococnv1 ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐴 ) )
46 45 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ 𝑔 ∘ 𝑔 ) = ( I ↾ 𝐴 ) )
47 46 coeq2d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) )
48 9 adantrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 )
49 f1of ⊢ ( ( ℎ ∘ 𝑥 ) : 𝐴 –1-1-onto→ 𝐷 → ( ℎ ∘ 𝑥 ) : 𝐴 ⟶ 𝐷 )
50 fcoi1 ⊢ ( ( ℎ ∘ 𝑥 ) : 𝐴 ⟶ 𝐷 → ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) = ( ℎ ∘ 𝑥 ) )
51 48 49 50 3syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( I ↾ 𝐴 ) ) = ( ℎ ∘ 𝑥 ) )
52 47 51 eqtrd ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ( ◡ 𝑔 ∘ 𝑔 ) ) = ( ℎ ∘ 𝑥 ) )
53 44 52 syl5req ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ 𝑥 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) )
54 coass ⊢ ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) )
55 f1ococnv2 ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ( ℎ ∘ ◡ ℎ ) = ( I ↾ 𝐷 ) )
56 55 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ ◡ ℎ ) = ( I ↾ 𝐷 ) )
57 56 coeq1d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) )
58 30 adantrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 )
59 f1of ⊢ ( ( 𝑦 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐷 → ( 𝑦 ∘ 𝑔 ) : 𝐴 ⟶ 𝐷 )
60 fcoi2 ⊢ ( ( 𝑦 ∘ 𝑔 ) : 𝐴 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
61 58 59 60 3syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( I ↾ 𝐷 ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
62 57 61 eqtrd ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ ◡ ℎ ) ∘ ( 𝑦 ∘ 𝑔 ) ) = ( 𝑦 ∘ 𝑔 ) )
63 54 62 eqtr3id ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) = ( 𝑦 ∘ 𝑔 ) )
64 53 63 eqeq12d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( 𝑦 ∘ 𝑔 ) ) )
65 eqcom ⊢ ( ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) = ( 𝑦 ∘ 𝑔 ) ↔ ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) )
66 64 65 bitrdi ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ) )
67 f1of1 ⊢ ( ℎ : 𝐶 –1-1-onto→ 𝐷 → ℎ : 𝐶 –1-1→ 𝐷 )
68 67 ad2antlr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ℎ : 𝐶 –1-1→ 𝐷 )
69 f1of ⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 → 𝑥 : 𝐴 ⟶ 𝐶 )
70 69 ad2antrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑥 : 𝐴 ⟶ 𝐶 )
71 32 adantrl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 )
72 f1of ⊢ ( ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 –1-1-onto→ 𝐶 → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 )
73 71 72 syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 )
74 cocan1 ⊢ ( ( ℎ : 𝐶 –1-1→ 𝐷 ∧ 𝑥 : 𝐴 ⟶ 𝐶 ∧ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) : 𝐴 ⟶ 𝐶 ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
75 68 70 73 74 syl3anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) = ( ℎ ∘ ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) ↔ 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ) )
76 f1ofo ⊢ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 → 𝑔 : 𝐴 –onto→ 𝐵 )
77 76 ad2antrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑔 : 𝐴 –onto→ 𝐵 )
78 f1ofn ⊢ ( 𝑦 : 𝐵 –1-1-onto→ 𝐷 → 𝑦 Fn 𝐵 )
79 78 ad2antll ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → 𝑦 Fn 𝐵 )
80 13 adantrr ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 )
81 f1ofn ⊢ ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) : 𝐵 –1-1-onto→ 𝐷 → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 )
82 80 81 syl ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 )
83 cocan2 ⊢ ( ( 𝑔 : 𝐴 –onto→ 𝐵 ∧ 𝑦 Fn 𝐵 ∧ ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) Fn 𝐵 ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
84 77 79 82 83 syl3anc ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( ( 𝑦 ∘ 𝑔 ) = ( ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ∘ 𝑔 ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
85 66 75 84 3bitr3d ⊢ ( ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) ∧ ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) )
86 85 ex ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 : 𝐴 –1-1-onto→ 𝐶 ∧ 𝑦 : 𝐵 –1-1-onto→ 𝐷 ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
87 43 86 syl5bi ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → ( ( 𝑥 ∈ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ∧ 𝑦 ∈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } ) → ( 𝑥 = ( ◡ ℎ ∘ ( 𝑦 ∘ 𝑔 ) ) ↔ 𝑦 = ( ( ℎ ∘ 𝑥 ) ∘ ◡ 𝑔 ) ) ) )
88 5 7 25 42 87 en3d ⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
89 88 exlimivv ⊢ ( ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
90 3 89 sylbir ⊢ ( ( ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ ℎ ℎ : 𝐶 –1-1-onto→ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )
91 1 2 90 syl2anb ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐶 } ≈ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐷 } )