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 ABCDf|f:A1-1 ontoCf|f:B1-1 ontoD

Proof

Step Hyp Ref Expression
1 bren ABgg:A1-1 ontoB
2 bren CDhh:C1-1 ontoD
3 exdistrv ghg:A1-1 ontoBh:C1-1 ontoDgg:A1-1 ontoBhh:C1-1 ontoD
4 f1osetex f|f:A1-1 ontoCV
5 4 a1i g:A1-1 ontoBh:C1-1 ontoDf|f:A1-1 ontoCV
6 f1osetex f|f:B1-1 ontoDV
7 6 a1i g:A1-1 ontoBh:C1-1 ontoDf|f:B1-1 ontoDV
8 f1oco h:C1-1 ontoDx:A1-1 ontoChx:A1-1 ontoD
9 8 adantll g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoChx:A1-1 ontoD
10 f1ocnv g:A1-1 ontoBg-1:B1-1 ontoA
11 10 ad2antrr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCg-1:B1-1 ontoA
12 f1oco hx:A1-1 ontoDg-1:B1-1 ontoAhxg-1:B1-1 ontoD
13 9 11 12 syl2anc g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoChxg-1:B1-1 ontoD
14 13 ex g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoChxg-1:B1-1 ontoD
15 vex xV
16 f1oeq1 f=xf:A1-1 ontoCx:A1-1 ontoC
17 15 16 elab xf|f:A1-1 ontoCx:A1-1 ontoC
18 vex hV
19 18 15 coex hxV
20 vex gV
21 20 cnvex g-1V
22 19 21 coex hxg-1V
23 f1oeq1 f=hxg-1f:B1-1 ontoDhxg-1:B1-1 ontoD
24 22 23 elab hxg-1f|f:B1-1 ontoDhxg-1:B1-1 ontoD
25 14 17 24 3imtr4g g:A1-1 ontoBh:C1-1 ontoDxf|f:A1-1 ontoChxg-1f|f:B1-1 ontoD
26 f1ocnv h:C1-1 ontoDh-1:D1-1 ontoC
27 26 ad2antlr g:A1-1 ontoBh:C1-1 ontoDy:B1-1 ontoDh-1:D1-1 ontoC
28 f1oco y:B1-1 ontoDg:A1-1 ontoByg:A1-1 ontoD
29 28 ancoms g:A1-1 ontoBy:B1-1 ontoDyg:A1-1 ontoD
30 29 adantlr g:A1-1 ontoBh:C1-1 ontoDy:B1-1 ontoDyg:A1-1 ontoD
31 f1oco h-1:D1-1 ontoCyg:A1-1 ontoDh-1yg:A1-1 ontoC
32 27 30 31 syl2anc g:A1-1 ontoBh:C1-1 ontoDy:B1-1 ontoDh-1yg:A1-1 ontoC
33 32 ex g:A1-1 ontoBh:C1-1 ontoDy:B1-1 ontoDh-1yg:A1-1 ontoC
34 vex yV
35 f1oeq1 f=yf:B1-1 ontoDy:B1-1 ontoD
36 34 35 elab yf|f:B1-1 ontoDy:B1-1 ontoD
37 18 cnvex h-1V
38 34 20 coex ygV
39 37 38 coex h-1ygV
40 f1oeq1 f=h-1ygf:A1-1 ontoCh-1yg:A1-1 ontoC
41 39 40 elab h-1ygf|f:A1-1 ontoCh-1yg:A1-1 ontoC
42 33 36 41 3imtr4g g:A1-1 ontoBh:C1-1 ontoDyf|f:B1-1 ontoDh-1ygf|f:A1-1 ontoC
43 17 36 anbi12i xf|f:A1-1 ontoCyf|f:B1-1 ontoDx:A1-1 ontoCy:B1-1 ontoD
44 coass hxg-1g=hxg-1g
45 f1ococnv1 g:A1-1 ontoBg-1g=IA
46 45 ad2antrr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDg-1g=IA
47 46 coeq2d g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhxg-1g=hxIA
48 9 adantrr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhx:A1-1 ontoD
49 f1of hx:A1-1 ontoDhx:AD
50 fcoi1 hx:ADhxIA=hx
51 48 49 50 3syl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhxIA=hx
52 47 51 eqtrd g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhxg-1g=hx
53 44 52 eqtr2id g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhx=hxg-1g
54 coass hh-1yg=hh-1yg
55 f1ococnv2 h:C1-1 ontoDhh-1=ID
56 55 ad2antlr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhh-1=ID
57 56 coeq1d g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhh-1yg=IDyg
58 30 adantrl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDyg:A1-1 ontoD
59 f1of yg:A1-1 ontoDyg:AD
60 fcoi2 yg:ADIDyg=yg
61 58 59 60 3syl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDIDyg=yg
62 57 61 eqtrd g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhh-1yg=yg
63 54 62 eqtr3id g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhh-1yg=yg
64 53 63 eqeq12d g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhx=hh-1yghxg-1g=yg
65 eqcom hxg-1g=ygyg=hxg-1g
66 64 65 bitrdi g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhx=hh-1ygyg=hxg-1g
67 f1of1 h:C1-1 ontoDh:C1-1D
68 67 ad2antlr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDh:C1-1D
69 f1of x:A1-1 ontoCx:AC
70 69 ad2antrl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDx:AC
71 32 adantrl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDh-1yg:A1-1 ontoC
72 f1of h-1yg:A1-1 ontoCh-1yg:AC
73 71 72 syl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDh-1yg:AC
74 cocan1 h:C1-1Dx:ACh-1yg:AChx=hh-1ygx=h-1yg
75 68 70 73 74 syl3anc g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhx=hh-1ygx=h-1yg
76 f1ofo g:A1-1 ontoBg:AontoB
77 76 ad2antrr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDg:AontoB
78 f1ofn y:B1-1 ontoDyFnB
79 78 ad2antll g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDyFnB
80 13 adantrr g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhxg-1:B1-1 ontoD
81 f1ofn hxg-1:B1-1 ontoDhxg-1FnB
82 80 81 syl g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDhxg-1FnB
83 cocan2 g:AontoByFnBhxg-1FnByg=hxg-1gy=hxg-1
84 77 79 82 83 syl3anc g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDyg=hxg-1gy=hxg-1
85 66 75 84 3bitr3d g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDx=h-1ygy=hxg-1
86 85 ex g:A1-1 ontoBh:C1-1 ontoDx:A1-1 ontoCy:B1-1 ontoDx=h-1ygy=hxg-1
87 43 86 syl5bi g:A1-1 ontoBh:C1-1 ontoDxf|f:A1-1 ontoCyf|f:B1-1 ontoDx=h-1ygy=hxg-1
88 5 7 25 42 87 en3d g:A1-1 ontoBh:C1-1 ontoDf|f:A1-1 ontoCf|f:B1-1 ontoD
89 88 exlimivv ghg:A1-1 ontoBh:C1-1 ontoDf|f:A1-1 ontoCf|f:B1-1 ontoD
90 3 89 sylbir gg:A1-1 ontoBhh:C1-1 ontoDf|f:A1-1 ontoCf|f:B1-1 ontoD
91 1 2 90 syl2anb ABCDf|f:A1-1 ontoCf|f:B1-1 ontoD