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 eqtr2id ( ( ( 𝑔 : 𝐴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𝐷 } )