Metamath Proof Explorer


Theorem catcisolem

Description: Lemma for catciso . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses catciso.c C = CatCat U
catciso.b B = Base C
catciso.r R = Base X
catciso.s S = Base Y
catciso.u φ U V
catciso.x φ X B
catciso.y φ Y B
catcisolem.i I = Inv C
catcisolem.g H = x S , y S F -1 x G F -1 y -1
catcisolem.1 φ F X Full Y X Faith Y G
catcisolem.2 φ F : R 1-1 onto S
Assertion catcisolem φ F G X I Y F -1 H

Proof

Step Hyp Ref Expression
1 catciso.c C = CatCat U
2 catciso.b B = Base C
3 catciso.r R = Base X
4 catciso.s S = Base Y
5 catciso.u φ U V
6 catciso.x φ X B
7 catciso.y φ Y B
8 catcisolem.i I = Inv C
9 catcisolem.g H = x S , y S F -1 x G F -1 y -1
10 catcisolem.1 φ F X Full Y X Faith Y G
11 catcisolem.2 φ F : R 1-1 onto S
12 f1ococnv1 F : R 1-1 onto S F -1 F = I R
13 11 12 syl φ F -1 F = I R
14 11 3ad2ant1 φ u R v R F : R 1-1 onto S
15 f1of F : R 1-1 onto S F : R S
16 14 15 syl φ u R v R F : R S
17 simp2 φ u R v R u R
18 16 17 ffvelrnd φ u R v R F u S
19 simp3 φ u R v R v R
20 16 19 ffvelrnd φ u R v R F v S
21 simpl x = F u y = F v x = F u
22 21 fveq2d x = F u y = F v F -1 x = F -1 F u
23 simpr x = F u y = F v y = F v
24 23 fveq2d x = F u y = F v F -1 y = F -1 F v
25 22 24 oveq12d x = F u y = F v F -1 x G F -1 y = F -1 F u G F -1 F v
26 25 cnveqd x = F u y = F v F -1 x G F -1 y -1 = F -1 F u G F -1 F v -1
27 ovex F -1 F u G F -1 F v V
28 27 cnvex F -1 F u G F -1 F v -1 V
29 26 9 28 ovmpoa F u S F v S F u H F v = F -1 F u G F -1 F v -1
30 18 20 29 syl2anc φ u R v R F u H F v = F -1 F u G F -1 F v -1
31 f1ocnvfv1 F : R 1-1 onto S u R F -1 F u = u
32 14 17 31 syl2anc φ u R v R F -1 F u = u
33 f1ocnvfv1 F : R 1-1 onto S v R F -1 F v = v
34 14 19 33 syl2anc φ u R v R F -1 F v = v
35 32 34 oveq12d φ u R v R F -1 F u G F -1 F v = u G v
36 35 cnveqd φ u R v R F -1 F u G F -1 F v -1 = u G v -1
37 30 36 eqtrd φ u R v R F u H F v = u G v -1
38 37 coeq1d φ u R v R F u H F v u G v = u G v -1 u G v
39 eqid Hom X = Hom X
40 eqid Hom Y = Hom Y
41 10 3ad2ant1 φ u R v R F X Full Y X Faith Y G
42 3 39 40 41 17 19 ffthf1o φ u R v R u G v : u Hom X v 1-1 onto F u Hom Y F v
43 f1ococnv1 u G v : u Hom X v 1-1 onto F u Hom Y F v u G v -1 u G v = I u Hom X v
44 42 43 syl φ u R v R u G v -1 u G v = I u Hom X v
45 38 44 eqtrd φ u R v R F u H F v u G v = I u Hom X v
46 45 mpoeq3dva φ u R , v R F u H F v u G v = u R , v R I u Hom X v
47 fveq2 z = u v Hom X z = Hom X u v
48 df-ov u Hom X v = Hom X u v
49 47 48 eqtr4di z = u v Hom X z = u Hom X v
50 49 reseq2d z = u v I Hom X z = I u Hom X v
51 50 mpompt z R × R I Hom X z = u R , v R I u Hom X v
52 46 51 eqtr4di φ u R , v R F u H F v u G v = z R × R I Hom X z
53 13 52 opeq12d φ F -1 F u R , v R F u H F v u G v = I R z R × R I Hom X z
54 inss1 X Full Y X Faith Y X Full Y
55 fullfunc X Full Y X Func Y
56 54 55 sstri X Full Y X Faith Y X Func Y
57 56 ssbri F X Full Y X Faith Y G F X Func Y G
58 10 57 syl φ F X Func Y G
59 eqid Id Y = Id Y
60 eqid Id X = Id X
61 eqid comp Y = comp Y
62 eqid comp X = comp X
63 1 2 5 catcbas φ B = U Cat
64 inss2 U Cat Cat
65 63 64 eqsstrdi φ B Cat
66 65 7 sseldd φ Y Cat
67 65 6 sseldd φ X Cat
68 f1ocnv F : R 1-1 onto S F -1 : S 1-1 onto R
69 f1of F -1 : S 1-1 onto R F -1 : S R
70 11 68 69 3syl φ F -1 : S R
71 ovex F -1 x G F -1 y V
72 71 cnvex F -1 x G F -1 y -1 V
73 9 72 fnmpoi H Fn S × S
74 73 a1i φ H Fn S × S
75 10 adantr φ u S v S F X Full Y X Faith Y G
76 70 ffvelrnda φ u S F -1 u R
77 76 adantrr φ u S v S F -1 u R
78 70 ffvelrnda φ v S F -1 v R
79 78 adantrl φ u S v S F -1 v R
80 3 39 40 75 77 79 ffthf1o φ u S v S F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v
81 f1ocnv F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v F -1 u G F -1 v -1 : F F -1 u Hom Y F F -1 v 1-1 onto F -1 u Hom X F -1 v
82 f1of F -1 u G F -1 v -1 : F F -1 u Hom Y F F -1 v 1-1 onto F -1 u Hom X F -1 v F -1 u G F -1 v -1 : F F -1 u Hom Y F F -1 v F -1 u Hom X F -1 v
83 80 81 82 3syl φ u S v S F -1 u G F -1 v -1 : F F -1 u Hom Y F F -1 v F -1 u Hom X F -1 v
84 simpl x = u y = v x = u
85 84 fveq2d x = u y = v F -1 x = F -1 u
86 simpr x = u y = v y = v
87 86 fveq2d x = u y = v F -1 y = F -1 v
88 85 87 oveq12d x = u y = v F -1 x G F -1 y = F -1 u G F -1 v
89 88 cnveqd x = u y = v F -1 x G F -1 y -1 = F -1 u G F -1 v -1
90 ovex F -1 u G F -1 v V
91 90 cnvex F -1 u G F -1 v -1 V
92 89 9 91 ovmpoa u S v S u H v = F -1 u G F -1 v -1
93 92 adantl φ u S v S u H v = F -1 u G F -1 v -1
94 11 adantr φ u S v S F : R 1-1 onto S
95 simprl φ u S v S u S
96 f1ocnvfv2 F : R 1-1 onto S u S F F -1 u = u
97 94 95 96 syl2anc φ u S v S F F -1 u = u
98 simprr φ u S v S v S
99 f1ocnvfv2 F : R 1-1 onto S v S F F -1 v = v
100 94 98 99 syl2anc φ u S v S F F -1 v = v
101 97 100 oveq12d φ u S v S F F -1 u Hom Y F F -1 v = u Hom Y v
102 101 eqcomd φ u S v S u Hom Y v = F F -1 u Hom Y F F -1 v
103 93 102 feq12d φ u S v S u H v : u Hom Y v F -1 u Hom X F -1 v F -1 u G F -1 v -1 : F F -1 u Hom Y F F -1 v F -1 u Hom X F -1 v
104 83 103 mpbird φ u S v S u H v : u Hom Y v F -1 u Hom X F -1 v
105 simpr φ u S u S
106 simpl x = u y = u x = u
107 106 fveq2d x = u y = u F -1 x = F -1 u
108 simpr x = u y = u y = u
109 108 fveq2d x = u y = u F -1 y = F -1 u
110 107 109 oveq12d x = u y = u F -1 x G F -1 y = F -1 u G F -1 u
111 110 cnveqd x = u y = u F -1 x G F -1 y -1 = F -1 u G F -1 u -1
112 ovex F -1 u G F -1 u V
113 112 cnvex F -1 u G F -1 u -1 V
114 111 9 113 ovmpoa u S u S u H u = F -1 u G F -1 u -1
115 105 105 114 syl2anc φ u S u H u = F -1 u G F -1 u -1
116 115 fveq1d φ u S u H u Id Y u = F -1 u G F -1 u -1 Id Y u
117 58 adantr φ u S F X Func Y G
118 3 60 59 117 76 funcid φ u S F -1 u G F -1 u Id X F -1 u = Id Y F F -1 u
119 11 96 sylan φ u S F F -1 u = u
120 119 fveq2d φ u S Id Y F F -1 u = Id Y u
121 118 120 eqtrd φ u S F -1 u G F -1 u Id X F -1 u = Id Y u
122 10 adantr φ u S F X Full Y X Faith Y G
123 3 39 40 122 76 76 ffthf1o φ u S F -1 u G F -1 u : F -1 u Hom X F -1 u 1-1 onto F F -1 u Hom Y F F -1 u
124 67 adantr φ u S X Cat
125 3 39 60 124 76 catidcl φ u S Id X F -1 u F -1 u Hom X F -1 u
126 f1ocnvfv F -1 u G F -1 u : F -1 u Hom X F -1 u 1-1 onto F F -1 u Hom Y F F -1 u Id X F -1 u F -1 u Hom X F -1 u F -1 u G F -1 u Id X F -1 u = Id Y u F -1 u G F -1 u -1 Id Y u = Id X F -1 u
127 123 125 126 syl2anc φ u S F -1 u G F -1 u Id X F -1 u = Id Y u F -1 u G F -1 u -1 Id Y u = Id X F -1 u
128 121 127 mpd φ u S F -1 u G F -1 u -1 Id Y u = Id X F -1 u
129 116 128 eqtrd φ u S u H u Id Y u = Id X F -1 u
130 58 3ad2ant1 φ u S v S z S f u Hom Y v g v Hom Y z F X Func Y G
131 70 3ad2ant1 φ u S v S z S f u Hom Y v g v Hom Y z F -1 : S R
132 simp21 φ u S v S z S f u Hom Y v g v Hom Y z u S
133 131 132 ffvelrnd φ u S v S z S f u Hom Y v g v Hom Y z F -1 u R
134 simp22 φ u S v S z S f u Hom Y v g v Hom Y z v S
135 131 134 ffvelrnd φ u S v S z S f u Hom Y v g v Hom Y z F -1 v R
136 simp23 φ u S v S z S f u Hom Y v g v Hom Y z z S
137 131 136 ffvelrnd φ u S v S z S f u Hom Y v g v Hom Y z F -1 z R
138 10 3ad2ant1 φ u S v S z S f u Hom Y v g v Hom Y z F X Full Y X Faith Y G
139 3 39 40 138 133 135 ffthf1o φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v
140 11 3ad2ant1 φ u S v S z S f u Hom Y v g v Hom Y z F : R 1-1 onto S
141 140 132 96 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F F -1 u = u
142 140 134 99 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F F -1 v = v
143 141 142 oveq12d φ u S v S z S f u Hom Y v g v Hom Y z F F -1 u Hom Y F F -1 v = u Hom Y v
144 143 f1oeq3d φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v
145 139 144 mpbid φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v
146 f1ocnv F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v F -1 u G F -1 v -1 : u Hom Y v 1-1 onto F -1 u Hom X F -1 v
147 f1of F -1 u G F -1 v -1 : u Hom Y v 1-1 onto F -1 u Hom X F -1 v F -1 u G F -1 v -1 : u Hom Y v F -1 u Hom X F -1 v
148 145 146 147 3syl φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v -1 : u Hom Y v F -1 u Hom X F -1 v
149 simp3l φ u S v S z S f u Hom Y v g v Hom Y z f u Hom Y v
150 148 149 ffvelrnd φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v -1 f F -1 u Hom X F -1 v
151 3 39 40 138 135 137 ffthf1o φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto F F -1 v Hom Y F F -1 z
152 f1ocnvfv2 F : R 1-1 onto S z S F F -1 z = z
153 140 136 152 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F F -1 z = z
154 142 153 oveq12d φ u S v S z S f u Hom Y v g v Hom Y z F F -1 v Hom Y F F -1 z = v Hom Y z
155 154 f1oeq3d φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto F F -1 v Hom Y F F -1 z F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto v Hom Y z
156 151 155 mpbid φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto v Hom Y z
157 f1ocnv F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto v Hom Y z F -1 v G F -1 z -1 : v Hom Y z 1-1 onto F -1 v Hom X F -1 z
158 f1of F -1 v G F -1 z -1 : v Hom Y z 1-1 onto F -1 v Hom X F -1 z F -1 v G F -1 z -1 : v Hom Y z F -1 v Hom X F -1 z
159 156 157 158 3syl φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z -1 : v Hom Y z F -1 v Hom X F -1 z
160 simp3r φ u S v S z S f u Hom Y v g v Hom Y z g v Hom Y z
161 159 160 ffvelrnd φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z -1 g F -1 v Hom X F -1 z
162 3 39 62 61 130 133 135 137 150 161 funcco φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f = F -1 v G F -1 z F -1 v G F -1 z -1 g F F -1 u F F -1 v comp Y F F -1 z F -1 u G F -1 v F -1 u G F -1 v -1 f
163 141 142 opeq12d φ u S v S z S f u Hom Y v g v Hom Y z F F -1 u F F -1 v = u v
164 163 153 oveq12d φ u S v S z S f u Hom Y v g v Hom Y z F F -1 u F F -1 v comp Y F F -1 z = u v comp Y z
165 f1ocnvfv2 F -1 v G F -1 z : F -1 v Hom X F -1 z 1-1 onto v Hom Y z g v Hom Y z F -1 v G F -1 z F -1 v G F -1 z -1 g = g
166 156 160 165 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z F -1 v G F -1 z -1 g = g
167 f1ocnvfv2 F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v f u Hom Y v F -1 u G F -1 v F -1 u G F -1 v -1 f = f
168 145 149 167 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 v F -1 u G F -1 v -1 f = f
169 164 166 168 oveq123d φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z F -1 v G F -1 z -1 g F F -1 u F F -1 v comp Y F F -1 z F -1 u G F -1 v F -1 u G F -1 v -1 f = g u v comp Y z f
170 162 169 eqtrd φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f = g u v comp Y z f
171 3 39 40 138 133 137 ffthf1o φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z : F -1 u Hom X F -1 z 1-1 onto F F -1 u Hom Y F F -1 z
172 141 153 oveq12d φ u S v S z S f u Hom Y v g v Hom Y z F F -1 u Hom Y F F -1 z = u Hom Y z
173 172 f1oeq3d φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z : F -1 u Hom X F -1 z 1-1 onto F F -1 u Hom Y F F -1 z F -1 u G F -1 z : F -1 u Hom X F -1 z 1-1 onto u Hom Y z
174 171 173 mpbid φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z : F -1 u Hom X F -1 z 1-1 onto u Hom Y z
175 67 3ad2ant1 φ u S v S z S f u Hom Y v g v Hom Y z X Cat
176 3 39 62 175 133 135 137 150 161 catcocl φ u S v S z S f u Hom Y v g v Hom Y z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f F -1 u Hom X F -1 z
177 f1ocnvfv F -1 u G F -1 z : F -1 u Hom X F -1 z 1-1 onto u Hom Y z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f F -1 u Hom X F -1 z F -1 u G F -1 z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f = g u v comp Y z f F -1 u G F -1 z -1 g u v comp Y z f = F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f
178 174 176 177 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f = g u v comp Y z f F -1 u G F -1 z -1 g u v comp Y z f = F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f
179 170 178 mpd φ u S v S z S f u Hom Y v g v Hom Y z F -1 u G F -1 z -1 g u v comp Y z f = F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f
180 simpl x = u y = z x = u
181 180 fveq2d x = u y = z F -1 x = F -1 u
182 simpr x = u y = z y = z
183 182 fveq2d x = u y = z F -1 y = F -1 z
184 181 183 oveq12d x = u y = z F -1 x G F -1 y = F -1 u G F -1 z
185 184 cnveqd x = u y = z F -1 x G F -1 y -1 = F -1 u G F -1 z -1
186 ovex F -1 u G F -1 z V
187 186 cnvex F -1 u G F -1 z -1 V
188 185 9 187 ovmpoa u S z S u H z = F -1 u G F -1 z -1
189 132 136 188 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z u H z = F -1 u G F -1 z -1
190 189 fveq1d φ u S v S z S f u Hom Y v g v Hom Y z u H z g u v comp Y z f = F -1 u G F -1 z -1 g u v comp Y z f
191 simpl x = v y = z x = v
192 191 fveq2d x = v y = z F -1 x = F -1 v
193 simpr x = v y = z y = z
194 193 fveq2d x = v y = z F -1 y = F -1 z
195 192 194 oveq12d x = v y = z F -1 x G F -1 y = F -1 v G F -1 z
196 195 cnveqd x = v y = z F -1 x G F -1 y -1 = F -1 v G F -1 z -1
197 ovex F -1 v G F -1 z V
198 197 cnvex F -1 v G F -1 z -1 V
199 196 9 198 ovmpoa v S z S v H z = F -1 v G F -1 z -1
200 134 136 199 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z v H z = F -1 v G F -1 z -1
201 200 fveq1d φ u S v S z S f u Hom Y v g v Hom Y z v H z g = F -1 v G F -1 z -1 g
202 132 134 92 syl2anc φ u S v S z S f u Hom Y v g v Hom Y z u H v = F -1 u G F -1 v -1
203 202 fveq1d φ u S v S z S f u Hom Y v g v Hom Y z u H v f = F -1 u G F -1 v -1 f
204 201 203 oveq12d φ u S v S z S f u Hom Y v g v Hom Y z v H z g F -1 u F -1 v comp X F -1 z u H v f = F -1 v G F -1 z -1 g F -1 u F -1 v comp X F -1 z F -1 u G F -1 v -1 f
205 179 190 204 3eqtr4d φ u S v S z S f u Hom Y v g v Hom Y z u H z g u v comp Y z f = v H z g F -1 u F -1 v comp X F -1 z u H v f
206 4 3 40 39 59 60 61 62 66 67 70 74 104 129 205 isfuncd φ F -1 Y Func X H
207 3 58 206 cofuval2 φ F -1 H func F G = F -1 F u R , v R F u H F v u G v
208 eqid id func X = id func X
209 208 3 67 39 idfuval φ id func X = I R z R × R I Hom X z
210 53 207 209 3eqtr4d φ F -1 H func F G = id func X
211 eqid comp C = comp C
212 df-br F X Func Y G F G X Func Y
213 58 212 sylib φ F G X Func Y
214 df-br F -1 Y Func X H F -1 H Y Func X
215 206 214 sylib φ F -1 H Y Func X
216 1 2 5 211 6 7 6 213 215 catcco φ F -1 H X Y comp C X F G = F -1 H func F G
217 eqid Id C = Id C
218 1 2 217 208 5 6 catcid φ Id C X = id func X
219 210 216 218 3eqtr4d φ F -1 H X Y comp C X F G = Id C X
220 eqid Hom C = Hom C
221 eqid Sect C = Sect C
222 1 catccat U V C Cat
223 5 222 syl φ C Cat
224 1 2 5 220 6 7 catchom φ X Hom C Y = X Func Y
225 213 224 eleqtrrd φ F G X Hom C Y
226 1 2 5 220 7 6 catchom φ Y Hom C X = Y Func X
227 215 226 eleqtrrd φ F -1 H Y Hom C X
228 2 220 211 217 221 223 6 7 225 227 issect2 φ F G X Sect C Y F -1 H F -1 H X Y comp C X F G = Id C X
229 219 228 mpbird φ F G X Sect C Y F -1 H
230 f1ococnv2 F : R 1-1 onto S F F -1 = I S
231 11 230 syl φ F F -1 = I S
232 92 3adant1 φ u S v S u H v = F -1 u G F -1 v -1
233 232 coeq2d φ u S v S F -1 u G F -1 v u H v = F -1 u G F -1 v F -1 u G F -1 v -1
234 10 3ad2ant1 φ u S v S F X Full Y X Faith Y G
235 76 3adant3 φ u S v S F -1 u R
236 78 3adant2 φ u S v S F -1 v R
237 3 39 40 234 235 236 ffthf1o φ u S v S F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v
238 101 3impb φ u S v S F F -1 u Hom Y F F -1 v = u Hom Y v
239 238 f1oeq3d φ u S v S F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto F F -1 u Hom Y F F -1 v F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v
240 237 239 mpbid φ u S v S F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v
241 f1ococnv2 F -1 u G F -1 v : F -1 u Hom X F -1 v 1-1 onto u Hom Y v F -1 u G F -1 v F -1 u G F -1 v -1 = I u Hom Y v
242 240 241 syl φ u S v S F -1 u G F -1 v F -1 u G F -1 v -1 = I u Hom Y v
243 233 242 eqtrd φ u S v S F -1 u G F -1 v u H v = I u Hom Y v
244 243 mpoeq3dva φ u S , v S F -1 u G F -1 v u H v = u S , v S I u Hom Y v
245 fveq2 z = u v Hom Y z = Hom Y u v
246 df-ov u Hom Y v = Hom Y u v
247 245 246 eqtr4di z = u v Hom Y z = u Hom Y v
248 247 reseq2d z = u v I Hom Y z = I u Hom Y v
249 248 mpompt z S × S I Hom Y z = u S , v S I u Hom Y v
250 244 249 eqtr4di φ u S , v S F -1 u G F -1 v u H v = z S × S I Hom Y z
251 231 250 opeq12d φ F F -1 u S , v S F -1 u G F -1 v u H v = I S z S × S I Hom Y z
252 4 206 58 cofuval2 φ F G func F -1 H = F F -1 u S , v S F -1 u G F -1 v u H v
253 eqid id func Y = id func Y
254 253 4 66 40 idfuval φ id func Y = I S z S × S I Hom Y z
255 251 252 254 3eqtr4d φ F G func F -1 H = id func Y
256 1 2 5 211 7 6 7 215 213 catcco φ F G Y X comp C Y F -1 H = F G func F -1 H
257 1 2 217 253 5 7 catcid φ Id C Y = id func Y
258 255 256 257 3eqtr4d φ F G Y X comp C Y F -1 H = Id C Y
259 2 220 211 217 221 223 7 6 227 225 issect2 φ F -1 H Y Sect C X F G F G Y X comp C Y F -1 H = Id C Y
260 258 259 mpbird φ F -1 H Y Sect C X F G
261 2 8 223 6 7 221 isinv φ F G X I Y F -1 H F G X Sect C Y F -1 H F -1 H Y Sect C X F G
262 229 260 261 mpbir2and φ F G X I Y F -1 H