Metamath Proof Explorer

Theorem hashfacenOLD

Description: Obsolete version of hashfacen as of 7-Aug-2024. (Contributed by Mario Carneiro, 21-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hashfacenOLD 
|- ( ( 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 f1of 
 |-  ( f : A -1-1-onto-> C -> f : A --> C )
5 f1odm 
 |-  ( h : C -1-1-onto-> D -> dom h = C )
6 vex 
 |-  h e. _V
7 6 dmex 
 |-  dom h e. _V
8 5 7 eqeltrrdi 
 |-  ( h : C -1-1-onto-> D -> C e. _V )
9 f1odm 
 |-  ( g : A -1-1-onto-> B -> dom g = A )
10 vex 
 |-  g e. _V
11 10 dmex 
 |-  dom g e. _V
12 9 11 eqeltrrdi 
 |-  ( g : A -1-1-onto-> B -> A e. _V )
13 elmapg 
 |-  ( ( C e. _V /\ A e. _V ) -> ( f e. ( C ^m A ) <-> f : A --> C ) )
14 8 12 13 syl2anr 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( f e. ( C ^m A ) <-> f : A --> C ) )
15 4 14 syl5ibr 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( f : A -1-1-onto-> C -> f e. ( C ^m A ) ) )
16 15 abssdv 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : A -1-1-onto-> C } C_ ( C ^m A ) )
17 ovex 
 |-  ( C ^m A ) e. _V
18 17 ssex 
 |-  ( { f | f : A -1-1-onto-> C } C_ ( C ^m A ) -> { f | f : A -1-1-onto-> C } e. _V )
19 16 18 syl 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : A -1-1-onto-> C } e. _V )
20 f1of 
 |-  ( f : B -1-1-onto-> D -> f : B --> D )
21 f1ofo 
 |-  ( h : C -1-1-onto-> D -> h : C -onto-> D )
22 forn 
 |-  ( h : C -onto-> D -> ran h = D )
23 21 22 syl 
 |-  ( h : C -1-1-onto-> D -> ran h = D )
24 6 rnex 
 |-  ran h e. _V
25 23 24 eqeltrrdi 
 |-  ( h : C -1-1-onto-> D -> D e. _V )
26 f1ofo 
 |-  ( g : A -1-1-onto-> B -> g : A -onto-> B )
27 forn 
 |-  ( g : A -onto-> B -> ran g = B )
28 26 27 syl 
 |-  ( g : A -1-1-onto-> B -> ran g = B )
29 10 rnex 
 |-  ran g e. _V
30 28 29 eqeltrrdi 
 |-  ( g : A -1-1-onto-> B -> B e. _V )
31 elmapg 
 |-  ( ( D e. _V /\ B e. _V ) -> ( f e. ( D ^m B ) <-> f : B --> D ) )
32 25 30 31 syl2anr 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( f e. ( D ^m B ) <-> f : B --> D ) )
33 20 32 syl5ibr 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> ( f : B -1-1-onto-> D -> f e. ( D ^m B ) ) )
34 33 abssdv 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : B -1-1-onto-> D } C_ ( D ^m B ) )
35 ovex 
 |-  ( D ^m B ) e. _V
36 35 ssex 
 |-  ( { f | f : B -1-1-onto-> D } C_ ( D ^m B ) -> { f | f : B -1-1-onto-> D } e. _V )
37 34 36 syl 
 |-  ( ( g : A -1-1-onto-> B /\ h : C -1-1-onto-> D ) -> { f | f : B -1-1-onto-> D } e. _V )
38 f1oco 
 |-  ( ( h : C -1-1-onto-> D /\ x : A -1-1-onto-> C ) -> ( h o. x ) : A -1-1-onto-> D )
39 38 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 )
40 f1ocnv 
 |-  ( g : A -1-1-onto-> B -> `' g : B -1-1-onto-> A )
41 40 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 )
42 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 )
43 39 41 42 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 )
44 43 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 ) )
45 vex 
 |-  x e. _V
46 f1oeq1 
 |-  ( f = x -> ( f : A -1-1-onto-> C <-> x : A -1-1-onto-> C ) )
47 45 46 elab 
 |-  ( x e. { f | f : A -1-1-onto-> C } <-> x : A -1-1-onto-> C )
48 6 45 coex 
 |-  ( h o. x ) e. _V
49 10 cnvex 
 |-  `' g e. _V
50 48 49 coex 
 |-  ( ( h o. x ) o. `' g ) e. _V
51 f1oeq1 
 |-  ( f = ( ( h o. x ) o. `' g ) -> ( f : B -1-1-onto-> D <-> ( ( h o. x ) o. `' g ) : B -1-1-onto-> D ) )
52 50 51 elab 
 |-  ( ( ( h o. x ) o. `' g ) e. { f | f : B -1-1-onto-> D } <-> ( ( h o. x ) o. `' g ) : B -1-1-onto-> D )
53 44 47 52 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 } ) )
54 f1ocnv 
 |-  ( h : C -1-1-onto-> D -> `' h : D -1-1-onto-> C )
55 54 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 )
56 f1oco 
 |-  ( ( y : B -1-1-onto-> D /\ g : A -1-1-onto-> B ) -> ( y o. g ) : A -1-1-onto-> D )
57 56 ancoms 
 |-  ( ( g : A -1-1-onto-> B /\ y : B -1-1-onto-> D ) -> ( y o. g ) : A -1-1-onto-> D )
58 57 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 )
59 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 )
60 55 58 59 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 )
61 60 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 ) )
62 vex 
 |-  y e. _V
63 f1oeq1 
 |-  ( f = y -> ( f : B -1-1-onto-> D <-> y : B -1-1-onto-> D ) )
64 62 63 elab 
 |-  ( y e. { f | f : B -1-1-onto-> D } <-> y : B -1-1-onto-> D )
65 6 cnvex 
 |-  `' h e. _V
66 62 10 coex 
 |-  ( y o. g ) e. _V
67 65 66 coex 
 |-  ( `' h o. ( y o. g ) ) e. _V
68 f1oeq1 
 |-  ( f = ( `' h o. ( y o. g ) ) -> ( f : A -1-1-onto-> C <-> ( `' h o. ( y o. g ) ) : A -1-1-onto-> C ) )
69 67 68 elab 
 |-  ( ( `' h o. ( y o. g ) ) e. { f | f : A -1-1-onto-> C } <-> ( `' h o. ( y o. g ) ) : A -1-1-onto-> C )
70 61 64 69 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 } ) )
71 47 64 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 ) )
72 coass 
 |-  ( ( ( h o. x ) o. `' g ) o. g ) = ( ( h o. x ) o. ( `' g o. g ) )
73 f1ococnv1 
 |-  ( g : A -1-1-onto-> B -> ( `' g o. g ) = ( _I |` A ) )
74 73 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 ) )
75 74 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 ) ) )
76 39 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 )
77 f1of 
 |-  ( ( h o. x ) : A -1-1-onto-> D -> ( h o. x ) : A --> D )
78 fcoi1 
 |-  ( ( h o. x ) : A --> D -> ( ( h o. x ) o. ( _I |` A ) ) = ( h o. x ) )
79 76 77 78 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 ) )
80 75 79 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 ) )
81 72 80 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 o. x ) = ( ( ( h o. x ) o. `' g ) o. g ) )
82 coass 
 |-  ( ( h o. `' h ) o. ( y o. g ) ) = ( h o. ( `' h o. ( y o. g ) ) )
83 f1ococnv2 
 |-  ( h : C -1-1-onto-> D -> ( h o. `' h ) = ( _I |` D ) )
84 83 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 ) )
85 84 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 ) ) )
86 58 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 )
87 f1of 
 |-  ( ( y o. g ) : A -1-1-onto-> D -> ( y o. g ) : A --> D )
88 fcoi2 
 |-  ( ( y o. g ) : A --> D -> ( ( _I |` D ) o. ( y o. g ) ) = ( y o. g ) )
89 86 87 88 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 ) )
90 85 89 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 ) )
91 82 90 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 ) )
92 81 91 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 ) ) )
93 eqcom 
 |-  ( ( ( ( h o. x ) o. `' g ) o. g ) = ( y o. g ) <-> ( y o. g ) = ( ( ( h o. x ) o. `' g ) o. g ) )
94 92 93 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 ) ) )
95 f1of1 
 |-  ( h : C -1-1-onto-> D -> h : C -1-1-> D )
96 95 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 )
97 f1of 
 |-  ( x : A -1-1-onto-> C -> x : A --> C )
98 97 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 )
99 60 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 )
100 f1of 
 |-  ( ( `' h o. ( y o. g ) ) : A -1-1-onto-> C -> ( `' h o. ( y o. g ) ) : A --> C )
101 99 100 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 )
102 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 ) ) ) )
103 96 98 101 102 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 ) ) ) )
104 26 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 )
105 f1ofn 
 |-  ( y : B -1-1-onto-> D -> y Fn B )
106 105 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 )
107 43 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 )
108 f1ofn 
 |-  ( ( ( h o. x ) o. `' g ) : B -1-1-onto-> D -> ( ( h o. x ) o. `' g ) Fn B )
109 107 108 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 )
110 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 ) ) )
111 104 106 109 110 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 ) ) )
112 94 103 111 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 ) ) )
113 112 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 ) ) ) )
114 71 113 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 ) ) ) )
115 19 37 53 70 114 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 } )
116 115 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 } )
117 3 116 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 } )
118 1 2 117 syl2anb 
 |-  ( ( A ~~ B /\ C ~~ D ) -> { f | f : A -1-1-onto-> C } ~~ { f | f : B -1-1-onto-> D } )