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 <-> E. g g : A -1-1-onto-> B )
2 bren 
 |-  ( C ~~ D <-> E. h h : C -1-1-onto-> D )
3 exdistrv 
 |-  ( E. g E. h ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) <-> ( E. g g : A -1-1-onto-> B /\ E. h h : C -1-1-onto-> D ) )
4 f1osetex 
 |-  { f | f : A -1-1-onto-> C } e. _V
5 4 a1i 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : A -1-1-onto-> C } e. _V )
6 f1osetex 
 |-  { f | f : B -1-1-onto-> D } e. _V
7 6 a1i 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : B -1-1-onto-> D } e. _V )
8 f1oco 
 |-  ( ( h : C -1-1-onto-> D /\ x : A -1-1-onto-> C ) -> ( h o. 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 o. x ) : A -1-1-onto-> D )
10 f1ocnv 
 |-  ( g : A -1-1-onto-> B -> `' g : 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 : B -1-1-onto-> A )
12 f1oco 
 |-  ( ( ( h o. x ) : A -1-1-onto-> D /\ `' g : B -1-1-onto-> A ) -> ( ( h o. x ) o. `' g ) : 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 o. x ) o. `' g ) : 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 o. x ) o. `' g ) : B -1-1-onto-> D ) )
15 vex 
 |-  x e. _V
16 f1oeq1 
 |-  ( f = x -> ( f : A -1-1-onto-> C <-> x : A -1-1-onto-> C ) )
17 15 16 elab 
 |-  ( x e. { f | f : A -1-1-onto-> C } <-> x : A -1-1-onto-> C )
18 vex 
 |-  h e. _V
19 18 15 coex 
 |-  ( h o. x ) e. _V
20 vex 
 |-  g e. _V
21 20 cnvex 
 |-  `' g e. _V
22 19 21 coex 
 |-  ( ( h o. x ) o. `' g ) e. _V
23 f1oeq1 
 |-  ( f = ( ( h o. x ) o. `' g ) -> ( f : B -1-1-onto-> D <-> ( ( h o. x ) o. `' g ) : B -1-1-onto-> D ) )
24 22 23 elab 
 |-  ( ( ( h o. x ) o. `' g ) e. { f | f : B -1-1-onto-> D } <-> ( ( h o. x ) o. `' g ) : B -1-1-onto-> D )
25 14 17 24 3imtr4g 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( x e. { f | f : A -1-1-onto-> C } -> ( ( h o. x ) o. `' g ) e. { f | f : B -1-1-onto-> D } ) )
26 f1ocnv 
 |-  ( h : C -1-1-onto-> D -> `' h : 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 : D -1-1-onto-> C )
28 f1oco 
 |-  ( ( y : B -1-1-onto-> D /\ g : A -1-1-onto-> B ) -> ( y o. g ) : A -1-1-onto-> D )
29 28 ancoms 
 |-  ( ( g : A -1-1-onto-> B /\ y : B -1-1-onto-> D ) -> ( y o. 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 o. g ) : A -1-1-onto-> D )
31 f1oco 
 |-  ( ( `' h : D -1-1-onto-> C /\ ( y o. g ) : A -1-1-onto-> D ) -> ( `' h o. ( y o. 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 o. ( y o. 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 o. ( y o. g ) ) : A -1-1-onto-> C ) )
34 vex 
 |-  y e. _V
35 f1oeq1 
 |-  ( f = y -> ( f : B -1-1-onto-> D <-> y : B -1-1-onto-> D ) )
36 34 35 elab 
 |-  ( y e. { f | f : B -1-1-onto-> D } <-> y : B -1-1-onto-> D )
37 18 cnvex 
 |-  `' h e. _V
38 34 20 coex 
 |-  ( y o. g ) e. _V
39 37 38 coex 
 |-  ( `' h o. ( y o. g ) ) e. _V
40 f1oeq1 
 |-  ( f = ( `' h o. ( y o. g ) ) -> ( f : A -1-1-onto-> C <-> ( `' h o. ( y o. g ) ) : A -1-1-onto-> C ) )
41 39 40 elab 
 |-  ( ( `' h o. ( y o. g ) ) e. { f | f : A -1-1-onto-> C } <-> ( `' h o. ( y o. g ) ) : A -1-1-onto-> C )
42 33 36 41 3imtr4g 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( y e. { f | f : B -1-1-onto-> D } -> ( `' h o. ( y o. g ) ) e. { f | f : A -1-1-onto-> C } ) )
43 17 36 anbi12i 
 |-  ( ( x e. { f | f : A -1-1-onto-> C } /\ y e. { f | f : B -1-1-onto-> D } ) <-> ( x : A -1-1-onto-> C /\ y : B -1-1-onto-> D ) )
44 coass 
 |-  ( ( ( h o. x ) o. `' g ) o. g ) = ( ( h o. x ) o. ( `' g o. g ) )
45 f1ococnv1 
 |-  ( g : A -1-1-onto-> B -> ( `' g o. 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 o. 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 o. x ) o. ( `' g o. g ) ) = ( ( h o. x ) o. ( _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 o. x ) : A -1-1-onto-> D )
49 f1of 
 |-  ( ( h o. x ) : A -1-1-onto-> D -> ( h o. x ) : A --> D )
50 fcoi1 
 |-  ( ( h o. x ) : A --> D -> ( ( h o. x ) o. ( _I |` A ) ) = ( h o. 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 o. x ) o. ( _I |` A ) ) = ( h o. 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 o. x ) o. ( `' g o. g ) ) = ( h o. x ) )
53 44 52 syl5req 
 |-  ( ( ( 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 o. x ) = ( ( ( h o. x ) o. `' g ) o. g ) )
54 coass 
 |-  ( ( h o. `' h ) o. ( y o. g ) ) = ( h o. ( `' h o. ( y o. g ) ) )
55 f1ococnv2 
 |-  ( h : C -1-1-onto-> D -> ( h o. `' h ) = ( _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 o. `' h ) = ( _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 o. `' h ) o. ( y o. g ) ) = ( ( _I |` D ) o. ( y o. 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 o. g ) : A -1-1-onto-> D )
59 f1of 
 |-  ( ( y o. g ) : A -1-1-onto-> D -> ( y o. g ) : A --> D )
60 fcoi2 
 |-  ( ( y o. g ) : A --> D -> ( ( _I |` D ) o. ( y o. g ) ) = ( y o. 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 ) o. ( y o. g ) ) = ( y o. 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 o. `' h ) o. ( y o. g ) ) = ( y o. 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 o. ( `' h o. ( y o. g ) ) ) = ( y o. 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 o. x ) = ( h o. ( `' h o. ( y o. g ) ) ) <-> ( ( ( h o. x ) o. `' g ) o. g ) = ( y o. g ) ) )
65 eqcom 
 |-  ( ( ( ( h o. x ) o. `' g ) o. g ) = ( y o. g ) <-> ( y o. g ) = ( ( ( h o. x ) o. `' g ) o. 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 o. x ) = ( h o. ( `' h o. ( y o. g ) ) ) <-> ( y o. g ) = ( ( ( h o. x ) o. `' g ) o. 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 o. ( y o. g ) ) : A -1-1-onto-> C )
72 f1of 
 |-  ( ( `' h o. ( y o. g ) ) : A -1-1-onto-> C -> ( `' h o. ( y o. 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 o. ( y o. g ) ) : A --> C )
74 cocan1 
 |-  ( ( h : C -1-1-> D /\ x : A --> C /\ ( `' h o. ( y o. g ) ) : A --> C ) -> ( ( h o. x ) = ( h o. ( `' h o. ( y o. g ) ) ) <-> x = ( `' h o. ( y o. 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 o. x ) = ( h o. ( `' h o. ( y o. g ) ) ) <-> x = ( `' h o. ( y o. 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 o. x ) o. `' g ) : B -1-1-onto-> D )
81 f1ofn 
 |-  ( ( ( h o. x ) o. `' g ) : B -1-1-onto-> D -> ( ( h o. x ) o. `' g ) 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 o. x ) o. `' g ) Fn B )
83 cocan2 
 |-  ( ( g : A -onto-> B /\ y Fn B /\ ( ( h o. x ) o. `' g ) Fn B ) -> ( ( y o. g ) = ( ( ( h o. x ) o. `' g ) o. g ) <-> y = ( ( h o. x ) o. `' g ) ) )
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 o. g ) = ( ( ( h o. x ) o. `' g ) o. g ) <-> y = ( ( h o. x ) o. `' g ) ) )
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 o. ( y o. g ) ) <-> y = ( ( h o. x ) o. `' g ) ) )
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 o. ( y o. g ) ) <-> y = ( ( h o. x ) o. `' g ) ) ) )
87 43 86 syl5bi 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( ( x e. { f | f : A -1-1-onto-> C } /\ y e. { f | f : B -1-1-onto-> D } ) -> ( x = ( `' h o. ( y o. g ) ) <-> y = ( ( h o. x ) o. `' g ) ) ) )
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 
 |-  ( E. g E. 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 
 |-  ( ( E. g g : A -1-1-onto-> B /\ E. 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 } )