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 A B C D f | f : A 1-1 onto C f | f : B 1-1 onto D

Proof

Step Hyp Ref Expression
1 bren A B g g : A 1-1 onto B
2 bren C D h h : C 1-1 onto D
3 exdistrv g h g : A 1-1 onto B h : C 1-1 onto D g g : A 1-1 onto B h h : C 1-1 onto D
4 f1osetex f | f : A 1-1 onto C V
5 4 a1i g : A 1-1 onto B h : C 1-1 onto D f | f : A 1-1 onto C V
6 f1osetex f | f : B 1-1 onto D V
7 6 a1i g : A 1-1 onto B h : C 1-1 onto D f | f : B 1-1 onto D V
8 f1oco h : C 1-1 onto D x : A 1-1 onto C h x : A 1-1 onto D
9 8 adantll g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C h x : A 1-1 onto D
10 f1ocnv g : A 1-1 onto B g -1 : B 1-1 onto A
11 10 ad2antrr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C g -1 : B 1-1 onto A
12 f1oco h x : A 1-1 onto D g -1 : B 1-1 onto A h x g -1 : B 1-1 onto D
13 9 11 12 syl2anc g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C h x g -1 : B 1-1 onto D
14 13 ex g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C h x g -1 : B 1-1 onto D
15 vex x V
16 f1oeq1 f = x f : A 1-1 onto C x : A 1-1 onto C
17 15 16 elab x f | f : A 1-1 onto C x : A 1-1 onto C
18 vex h V
19 18 15 coex h x V
20 vex g V
21 20 cnvex g -1 V
22 19 21 coex h x g -1 V
23 f1oeq1 f = h x g -1 f : B 1-1 onto D h x g -1 : B 1-1 onto D
24 22 23 elab h x g -1 f | f : B 1-1 onto D h x g -1 : B 1-1 onto D
25 14 17 24 3imtr4g g : A 1-1 onto B h : C 1-1 onto D x f | f : A 1-1 onto C h x g -1 f | f : B 1-1 onto D
26 f1ocnv h : C 1-1 onto D h -1 : D 1-1 onto C
27 26 ad2antlr g : A 1-1 onto B h : C 1-1 onto D y : B 1-1 onto D h -1 : D 1-1 onto C
28 f1oco y : B 1-1 onto D g : A 1-1 onto B y g : A 1-1 onto D
29 28 ancoms g : A 1-1 onto B y : B 1-1 onto D y g : A 1-1 onto D
30 29 adantlr g : A 1-1 onto B h : C 1-1 onto D y : B 1-1 onto D y g : A 1-1 onto D
31 f1oco h -1 : D 1-1 onto C y g : A 1-1 onto D h -1 y g : A 1-1 onto C
32 27 30 31 syl2anc g : A 1-1 onto B h : C 1-1 onto D y : B 1-1 onto D h -1 y g : A 1-1 onto C
33 32 ex g : A 1-1 onto B h : C 1-1 onto D y : B 1-1 onto D h -1 y g : A 1-1 onto C
34 vex y V
35 f1oeq1 f = y f : B 1-1 onto D y : B 1-1 onto D
36 34 35 elab y f | f : B 1-1 onto D y : B 1-1 onto D
37 18 cnvex h -1 V
38 34 20 coex y g V
39 37 38 coex h -1 y g V
40 f1oeq1 f = h -1 y g f : A 1-1 onto C h -1 y g : A 1-1 onto C
41 39 40 elab h -1 y g f | f : A 1-1 onto C h -1 y g : A 1-1 onto C
42 33 36 41 3imtr4g g : A 1-1 onto B h : C 1-1 onto D y f | f : B 1-1 onto D h -1 y g f | f : A 1-1 onto C
43 17 36 anbi12i x f | f : A 1-1 onto C y f | f : B 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D
44 coass h x g -1 g = h x g -1 g
45 f1ococnv1 g : A 1-1 onto B g -1 g = I A
46 45 ad2antrr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D g -1 g = I A
47 46 coeq2d g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x g -1 g = h x I A
48 9 adantrr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x : A 1-1 onto D
49 f1of h x : A 1-1 onto D h x : A D
50 fcoi1 h x : A D h x I A = h x
51 48 49 50 3syl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x I A = h x
52 47 51 eqtrd g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x g -1 g = h x
53 44 52 eqtr2id g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x = h x g -1 g
54 coass h h -1 y g = h h -1 y g
55 f1ococnv2 h : C 1-1 onto D h h -1 = I D
56 55 ad2antlr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h h -1 = I D
57 56 coeq1d g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h h -1 y g = I D y g
58 30 adantrl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D y g : A 1-1 onto D
59 f1of y g : A 1-1 onto D y g : A D
60 fcoi2 y g : A D I D y g = y g
61 58 59 60 3syl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D I D y g = y g
62 57 61 eqtrd g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h h -1 y g = y g
63 54 62 eqtr3id g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h h -1 y g = y g
64 53 63 eqeq12d g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x = h h -1 y g h x g -1 g = y g
65 eqcom h x g -1 g = y g y g = h x g -1 g
66 64 65 bitrdi g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x = h h -1 y g y g = h x g -1 g
67 f1of1 h : C 1-1 onto D h : C 1-1 D
68 67 ad2antlr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h : C 1-1 D
69 f1of x : A 1-1 onto C x : A C
70 69 ad2antrl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D x : A C
71 32 adantrl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h -1 y g : A 1-1 onto C
72 f1of h -1 y g : A 1-1 onto C h -1 y g : A C
73 71 72 syl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h -1 y g : A C
74 cocan1 h : C 1-1 D x : A C h -1 y g : A C h x = h h -1 y g x = h -1 y g
75 68 70 73 74 syl3anc g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x = h h -1 y g x = h -1 y g
76 f1ofo g : A 1-1 onto B g : A onto B
77 76 ad2antrr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D g : A onto B
78 f1ofn y : B 1-1 onto D y Fn B
79 78 ad2antll g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D y Fn B
80 13 adantrr g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x g -1 : B 1-1 onto D
81 f1ofn h x g -1 : B 1-1 onto D h x g -1 Fn B
82 80 81 syl g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D h x g -1 Fn B
83 cocan2 g : A onto B y Fn B h x g -1 Fn B y g = h x g -1 g y = h x g -1
84 77 79 82 83 syl3anc g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D y g = h x g -1 g y = h x g -1
85 66 75 84 3bitr3d g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D x = h -1 y g y = h x g -1
86 85 ex g : A 1-1 onto B h : C 1-1 onto D x : A 1-1 onto C y : B 1-1 onto D x = h -1 y g y = h x g -1
87 43 86 syl5bi g : A 1-1 onto B h : C 1-1 onto D x f | f : A 1-1 onto C y f | f : B 1-1 onto D x = h -1 y g y = h x g -1
88 5 7 25 42 87 en3d g : A 1-1 onto B h : C 1-1 onto D f | f : A 1-1 onto C f | f : B 1-1 onto D
89 88 exlimivv g h g : A 1-1 onto B h : C 1-1 onto D f | f : A 1-1 onto C f | f : B 1-1 onto D
90 3 89 sylbir g g : A 1-1 onto B h h : C 1-1 onto D f | f : A 1-1 onto C f | f : B 1-1 onto D
91 1 2 90 syl2anb A B C D f | f : A 1-1 onto C f | f : B 1-1 onto D