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 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 f1of f : A 1-1 onto C f : A C
5 f1odm h : C 1-1 onto D dom h = C
6 vex h V
7 6 dmex dom h V
8 5 7 eqeltrrdi h : C 1-1 onto D C V
9 f1odm g : A 1-1 onto B dom g = A
10 vex g V
11 10 dmex dom g V
12 9 11 eqeltrrdi g : A 1-1 onto B A V
13 elmapg C V A V f C A f : A C
14 8 12 13 syl2anr g : A 1-1 onto B h : C 1-1 onto D f C 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 C A
16 15 abssdv g : A 1-1 onto B h : C 1-1 onto D f | f : A 1-1 onto C C A
17 ovex C A V
18 17 ssex f | f : A 1-1 onto C C A f | f : A 1-1 onto C V
19 16 18 syl g : A 1-1 onto B h : C 1-1 onto D f | f : A 1-1 onto C 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 V
25 23 24 eqeltrrdi h : C 1-1 onto D D 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 V
30 28 29 eqeltrrdi g : A 1-1 onto B B V
31 elmapg D V B V f D B f : B D
32 25 30 31 syl2anr g : A 1-1 onto B h : C 1-1 onto D f D 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 D B
34 33 abssdv g : A 1-1 onto B h : C 1-1 onto D f | f : B 1-1 onto D D B
35 ovex D B V
36 35 ssex f | f : B 1-1 onto D D B f | f : B 1-1 onto D V
37 34 36 syl g : A 1-1 onto B h : C 1-1 onto D f | f : B 1-1 onto D V
38 f1oco h : C 1-1 onto D x : A 1-1 onto C h 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 x : A 1-1 onto D
40 f1ocnv g : A 1-1 onto B g -1 : 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 -1 : B 1-1 onto A
42 f1oco h x : A 1-1 onto D g -1 : B 1-1 onto A h x g -1 : 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 x g -1 : 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 x g -1 : B 1-1 onto D
45 vex x V
46 f1oeq1 f = x f : A 1-1 onto C x : A 1-1 onto C
47 45 46 elab x f | f : A 1-1 onto C x : A 1-1 onto C
48 6 45 coex h x V
49 10 cnvex g -1 V
50 48 49 coex h x g -1 V
51 f1oeq1 f = h x g -1 f : B 1-1 onto D h x g -1 : B 1-1 onto D
52 50 51 elab h x g -1 f | f : B 1-1 onto D h x g -1 : B 1-1 onto D
53 44 47 52 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
54 f1ocnv h : C 1-1 onto D h -1 : 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 -1 : D 1-1 onto C
56 f1oco y : B 1-1 onto D g : A 1-1 onto B y g : A 1-1 onto D
57 56 ancoms g : A 1-1 onto B y : B 1-1 onto D y 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 g : A 1-1 onto D
59 f1oco h -1 : D 1-1 onto C y g : A 1-1 onto D h -1 y 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 -1 y 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 -1 y g : A 1-1 onto C
62 vex y V
63 f1oeq1 f = y f : B 1-1 onto D y : B 1-1 onto D
64 62 63 elab y f | f : B 1-1 onto D y : B 1-1 onto D
65 6 cnvex h -1 V
66 62 10 coex y g V
67 65 66 coex h -1 y g V
68 f1oeq1 f = h -1 y g f : A 1-1 onto C h -1 y g : A 1-1 onto C
69 67 68 elab h -1 y g f | f : A 1-1 onto C h -1 y g : A 1-1 onto C
70 61 64 69 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
71 47 64 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
72 coass h x g -1 g = h x g -1 g
73 f1ococnv1 g : A 1-1 onto B g -1 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 -1 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 x g -1 g = h x 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 x : A 1-1 onto D
77 f1of h x : A 1-1 onto D h x : A D
78 fcoi1 h x : A D h x I A = h 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 x I A = h 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 x g -1 g = h 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 x = h x g -1 g
82 coass h h -1 y g = h h -1 y g
83 f1ococnv2 h : C 1-1 onto D h h -1 = 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 h -1 = 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 h -1 y g = I D y 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 g : A 1-1 onto D
87 f1of y g : A 1-1 onto D y g : A D
88 fcoi2 y g : A D I D y g = y 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 y g = y 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 h -1 y g = y 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 h -1 y g = y 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 x = h h -1 y g h x g -1 g = y g
93 eqcom h x g -1 g = y g y g = h x g -1 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 x = h h -1 y g y g = h x g -1 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 -1 y g : A 1-1 onto C
100 f1of h -1 y g : A 1-1 onto C h -1 y 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 -1 y g : A C
102 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
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 x = h h -1 y g x = h -1 y 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 x g -1 : B 1-1 onto D
108 f1ofn h x g -1 : B 1-1 onto D h x g -1 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 x g -1 Fn B
110 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
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 g = h x g -1 g y = h x g -1
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 -1 y g y = h x g -1
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 -1 y g y = h x g -1
114 71 113 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
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 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
117 3 116 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
118 1 2 117 syl2anb A B C D f | f : A 1-1 onto C f | f : B 1-1 onto D