Metamath Proof Explorer


Theorem cvmlift2lem9

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Hypotheses cvmlift2.b B = C
cvmlift2.f φ F C CovMap J
cvmlift2.g φ G II × t II Cn J
cvmlift2.p φ P B
cvmlift2.i φ F P = 0 G 0
cvmlift2.h H = ι f II Cn C | F f = z 0 1 z G 0 f 0 = P
cvmlift2.k K = x 0 1 , y 0 1 ι f II Cn C | F f = z 0 1 x G z f 0 = H x y
cvmlift2lem10.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
cvmlift2lem9.1 φ X G Y M
cvmlift2lem9.2 φ T S M
cvmlift2lem9.3 φ U II
cvmlift2lem9.4 φ V II
cvmlift2lem9.5 φ II 𝑡 U Conn
cvmlift2lem9.6 φ II 𝑡 V Conn
cvmlift2lem9.7 φ X U
cvmlift2lem9.8 φ Y V
cvmlift2lem9.9 φ U × V G -1 M
cvmlift2lem9.10 φ Z V
cvmlift2lem9.11 φ K U × Z II × t II 𝑡 U × Z Cn C
cvmlift2lem9.w W = ι b T | X K Y b
Assertion cvmlift2lem9 φ K U × V II × t II 𝑡 U × V Cn C

Proof

Step Hyp Ref Expression
1 cvmlift2.b B = C
2 cvmlift2.f φ F C CovMap J
3 cvmlift2.g φ G II × t II Cn J
4 cvmlift2.p φ P B
5 cvmlift2.i φ F P = 0 G 0
6 cvmlift2.h H = ι f II Cn C | F f = z 0 1 z G 0 f 0 = P
7 cvmlift2.k K = x 0 1 , y 0 1 ι f II Cn C | F f = z 0 1 x G z f 0 = H x y
8 cvmlift2lem10.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
9 cvmlift2lem9.1 φ X G Y M
10 cvmlift2lem9.2 φ T S M
11 cvmlift2lem9.3 φ U II
12 cvmlift2lem9.4 φ V II
13 cvmlift2lem9.5 φ II 𝑡 U Conn
14 cvmlift2lem9.6 φ II 𝑡 V Conn
15 cvmlift2lem9.7 φ X U
16 cvmlift2lem9.8 φ Y V
17 cvmlift2lem9.9 φ U × V G -1 M
18 cvmlift2lem9.10 φ Z V
19 cvmlift2lem9.11 φ K U × Z II × t II 𝑡 U × Z Cn C
20 cvmlift2lem9.w W = ι b T | X K Y b
21 iitop II Top
22 iiuni 0 1 = II
23 21 21 22 22 txunii 0 1 × 0 1 = II × t II
24 1 2 3 4 5 6 7 cvmlift2lem5 φ K : 0 1 × 0 1 B
25 1 2 3 4 5 6 7 cvmlift2lem7 φ F K = G
26 25 3 eqeltrd φ F K II × t II Cn J
27 21 21 txtopi II × t II Top
28 27 a1i φ II × t II Top
29 elssuni U II U II
30 29 22 sseqtrrdi U II U 0 1
31 11 30 syl φ U 0 1
32 31 15 sseldd φ X 0 1
33 elssuni V II V II
34 33 22 sseqtrrdi V II V 0 1
35 12 34 syl φ V 0 1
36 35 16 sseldd φ Y 0 1
37 opelxpi X 0 1 Y 0 1 X Y 0 1 × 0 1
38 32 36 37 syl2anc φ X Y 0 1 × 0 1
39 24 32 36 fovrnd φ X K Y B
40 fvco3 K : 0 1 × 0 1 B X Y 0 1 × 0 1 F K X Y = F K X Y
41 24 38 40 syl2anc φ F K X Y = F K X Y
42 25 fveq1d φ F K X Y = G X Y
43 41 42 eqtr3d φ F K X Y = G X Y
44 df-ov X K Y = K X Y
45 44 fveq2i F X K Y = F K X Y
46 df-ov X G Y = G X Y
47 43 45 46 3eqtr4g φ F X K Y = X G Y
48 47 9 eqeltrd φ F X K Y M
49 8 1 20 cvmsiota F C CovMap J T S M X K Y B F X K Y M W T X K Y W
50 2 10 39 48 49 syl13anc φ W T X K Y W
51 44 eleq1i X K Y W K X Y W
52 51 anbi2i W T X K Y W W T K X Y W
53 50 52 sylib φ W T K X Y W
54 xpss12 U 0 1 V 0 1 U × V 0 1 × 0 1
55 31 35 54 syl2anc φ U × V 0 1 × 0 1
56 snidg m U m m
57 56 ad2antrl φ m U n V m m
58 simprr φ m U n V n V
59 ovres m m n V m K m × V n = m K n
60 57 58 59 syl2anc φ m U n V m K m × V n = m K n
61 eqid II × t II 𝑡 m × V = II × t II 𝑡 m × V
62 21 a1i φ m U n V II Top
63 snex m V
64 63 a1i φ m U n V m V
65 12 adantr φ m U n V V II
66 txrest II Top II Top m V V II II × t II 𝑡 m × V = II 𝑡 m × t II 𝑡 V
67 62 62 64 65 66 syl22anc φ m U n V II × t II 𝑡 m × V = II 𝑡 m × t II 𝑡 V
68 iitopon II TopOn 0 1
69 31 sselda φ m U m 0 1
70 69 adantrr φ m U n V m 0 1
71 restsn2 II TopOn 0 1 m 0 1 II 𝑡 m = 𝒫 m
72 68 70 71 sylancr φ m U n V II 𝑡 m = 𝒫 m
73 pwsn 𝒫 m = m
74 indisconn m Conn
75 73 74 eqeltri 𝒫 m Conn
76 72 75 eqeltrdi φ m U n V II 𝑡 m Conn
77 14 adantr φ m U n V II 𝑡 V Conn
78 txconn II 𝑡 m Conn II 𝑡 V Conn II 𝑡 m × t II 𝑡 V Conn
79 76 77 78 syl2anc φ m U n V II 𝑡 m × t II 𝑡 V Conn
80 67 79 eqeltrd φ m U n V II × t II 𝑡 m × V Conn
81 1 2 3 4 5 6 7 cvmlift2lem6 φ m 0 1 K m × 0 1 II × t II 𝑡 m × 0 1 Cn C
82 70 81 syldan φ m U n V K m × 0 1 II × t II 𝑡 m × 0 1 Cn C
83 35 adantr φ m U n V V 0 1
84 xpss2 V 0 1 m × V m × 0 1
85 83 84 syl φ m U n V m × V m × 0 1
86 70 snssd φ m U n V m 0 1
87 xpss1 m 0 1 m × 0 1 0 1 × 0 1
88 86 87 syl φ m U n V m × 0 1 0 1 × 0 1
89 23 restuni II × t II Top m × 0 1 0 1 × 0 1 m × 0 1 = II × t II 𝑡 m × 0 1
90 27 88 89 sylancr φ m U n V m × 0 1 = II × t II 𝑡 m × 0 1
91 85 90 sseqtrd φ m U n V m × V II × t II 𝑡 m × 0 1
92 eqid II × t II 𝑡 m × 0 1 = II × t II 𝑡 m × 0 1
93 92 cnrest K m × 0 1 II × t II 𝑡 m × 0 1 Cn C m × V II × t II 𝑡 m × 0 1 K m × 0 1 m × V II × t II 𝑡 m × 0 1 𝑡 m × V Cn C
94 82 91 93 syl2anc φ m U n V K m × 0 1 m × V II × t II 𝑡 m × 0 1 𝑡 m × V Cn C
95 85 resabs1d φ m U n V K m × 0 1 m × V = K m × V
96 27 a1i φ m U n V II × t II Top
97 ovex 0 1 V
98 63 97 xpex m × 0 1 V
99 98 a1i φ m U n V m × 0 1 V
100 restabs II × t II Top m × V m × 0 1 m × 0 1 V II × t II 𝑡 m × 0 1 𝑡 m × V = II × t II 𝑡 m × V
101 96 85 99 100 syl3anc φ m U n V II × t II 𝑡 m × 0 1 𝑡 m × V = II × t II 𝑡 m × V
102 101 oveq1d φ m U n V II × t II 𝑡 m × 0 1 𝑡 m × V Cn C = II × t II 𝑡 m × V Cn C
103 94 95 102 3eltr3d φ m U n V K m × V II × t II 𝑡 m × V Cn C
104 cvmtop1 F C CovMap J C Top
105 2 104 syl φ C Top
106 105 adantr φ m U n V C Top
107 1 toptopon C Top C TopOn B
108 106 107 sylib φ m U n V C TopOn B
109 df-ima K m × V = ran K m × V
110 simprl φ m U n V m U
111 110 snssd φ m U n V m U
112 xpss1 m U m × V U × V
113 imass2 m × V U × V K m × V K U × V
114 111 112 113 3syl φ m U n V K m × V K U × V
115 imaco K -1 F -1 M = K -1 F -1 M
116 cnvco F K -1 = K -1 F -1
117 25 cnveqd φ F K -1 = G -1
118 116 117 eqtr3id φ K -1 F -1 = G -1
119 118 imaeq1d φ K -1 F -1 M = G -1 M
120 115 119 eqtr3id φ K -1 F -1 M = G -1 M
121 17 120 sseqtrrd φ U × V K -1 F -1 M
122 24 ffund φ Fun K
123 24 fdmd φ dom K = 0 1 × 0 1
124 55 123 sseqtrrd φ U × V dom K
125 funimass3 Fun K U × V dom K K U × V F -1 M U × V K -1 F -1 M
126 122 124 125 syl2anc φ K U × V F -1 M U × V K -1 F -1 M
127 121 126 mpbird φ K U × V F -1 M
128 127 adantr φ m U n V K U × V F -1 M
129 114 128 sstrd φ m U n V K m × V F -1 M
130 109 129 eqsstrrid φ m U n V ran K m × V F -1 M
131 cnvimass F -1 M dom F
132 cvmcn F C CovMap J F C Cn J
133 2 132 syl φ F C Cn J
134 eqid J = J
135 1 134 cnf F C Cn J F : B J
136 fdm F : B J dom F = B
137 133 135 136 3syl φ dom F = B
138 131 137 sseqtrid φ F -1 M B
139 138 adantr φ m U n V F -1 M B
140 cnrest2 C TopOn B ran K m × V F -1 M F -1 M B K m × V II × t II 𝑡 m × V Cn C K m × V II × t II 𝑡 m × V Cn C 𝑡 F -1 M
141 108 130 139 140 syl3anc φ m U n V K m × V II × t II 𝑡 m × V Cn C K m × V II × t II 𝑡 m × V Cn C 𝑡 F -1 M
142 103 141 mpbid φ m U n V K m × V II × t II 𝑡 m × V Cn C 𝑡 F -1 M
143 8 cvmsss T S M T C
144 10 143 syl φ T C
145 50 simpld φ W T
146 144 145 sseldd φ W C
147 elssuni W T W T
148 145 147 syl φ W T
149 8 cvmsuni T S M T = F -1 M
150 10 149 syl φ T = F -1 M
151 148 150 sseqtrd φ W F -1 M
152 8 cvmsrcl T S M M J
153 10 152 syl φ M J
154 cnima F C Cn J M J F -1 M C
155 133 153 154 syl2anc φ F -1 M C
156 restopn2 C Top F -1 M C W C 𝑡 F -1 M W C W F -1 M
157 105 155 156 syl2anc φ W C 𝑡 F -1 M W C W F -1 M
158 146 151 157 mpbir2and φ W C 𝑡 F -1 M
159 158 adantr φ m U n V W C 𝑡 F -1 M
160 8 cvmscld F C CovMap J T S M W T W Clsd C 𝑡 F -1 M
161 2 10 145 160 syl3anc φ W Clsd C 𝑡 F -1 M
162 161 adantr φ m U n V W Clsd C 𝑡 F -1 M
163 18 adantr φ m U n V Z V
164 opelxpi m m Z V m Z m × V
165 57 163 164 syl2anc φ m U n V m Z m × V
166 85 88 sstrd φ m U n V m × V 0 1 × 0 1
167 23 restuni II × t II Top m × V 0 1 × 0 1 m × V = II × t II 𝑡 m × V
168 27 166 167 sylancr φ m U n V m × V = II × t II 𝑡 m × V
169 165 168 eleqtrd φ m U n V m Z II × t II 𝑡 m × V
170 df-ov m K m × V Z = K m × V m Z
171 ovres m m Z V m K m × V Z = m K Z
172 57 163 171 syl2anc φ m U n V m K m × V Z = m K Z
173 snidg Z V Z Z
174 18 173 syl φ Z Z
175 174 adantr φ m U n V Z Z
176 ovres m U Z Z m K U × Z Z = m K Z
177 110 175 176 syl2anc φ m U n V m K U × Z Z = m K Z
178 172 177 eqtr4d φ m U n V m K m × V Z = m K U × Z Z
179 170 178 eqtr3id φ m U n V K m × V m Z = m K U × Z Z
180 eqid II × t II 𝑡 U × Z = II × t II 𝑡 U × Z
181 21 a1i φ II Top
182 snex Z V
183 182 a1i φ Z V
184 txrest II Top II Top U II Z V II × t II 𝑡 U × Z = II 𝑡 U × t II 𝑡 Z
185 181 181 11 183 184 syl22anc φ II × t II 𝑡 U × Z = II 𝑡 U × t II 𝑡 Z
186 35 18 sseldd φ Z 0 1
187 restsn2 II TopOn 0 1 Z 0 1 II 𝑡 Z = 𝒫 Z
188 68 186 187 sylancr φ II 𝑡 Z = 𝒫 Z
189 pwsn 𝒫 Z = Z
190 indisconn Z Conn
191 189 190 eqeltri 𝒫 Z Conn
192 188 191 eqeltrdi φ II 𝑡 Z Conn
193 txconn II 𝑡 U Conn II 𝑡 Z Conn II 𝑡 U × t II 𝑡 Z Conn
194 13 192 193 syl2anc φ II 𝑡 U × t II 𝑡 Z Conn
195 185 194 eqeltrd φ II × t II 𝑡 U × Z Conn
196 105 107 sylib φ C TopOn B
197 df-ima K U × Z = ran K U × Z
198 18 snssd φ Z V
199 xpss2 Z V U × Z U × V
200 imass2 U × Z U × V K U × Z K U × V
201 198 199 200 3syl φ K U × Z K U × V
202 201 127 sstrd φ K U × Z F -1 M
203 197 202 eqsstrrid φ ran K U × Z F -1 M
204 cnrest2 C TopOn B ran K U × Z F -1 M F -1 M B K U × Z II × t II 𝑡 U × Z Cn C K U × Z II × t II 𝑡 U × Z Cn C 𝑡 F -1 M
205 196 203 138 204 syl3anc φ K U × Z II × t II 𝑡 U × Z Cn C K U × Z II × t II 𝑡 U × Z Cn C 𝑡 F -1 M
206 19 205 mpbid φ K U × Z II × t II 𝑡 U × Z Cn C 𝑡 F -1 M
207 opelxpi X U Z Z X Z U × Z
208 15 174 207 syl2anc φ X Z U × Z
209 186 snssd φ Z 0 1
210 xpss12 U 0 1 Z 0 1 U × Z 0 1 × 0 1
211 31 209 210 syl2anc φ U × Z 0 1 × 0 1
212 23 restuni II × t II Top U × Z 0 1 × 0 1 U × Z = II × t II 𝑡 U × Z
213 27 211 212 sylancr φ U × Z = II × t II 𝑡 U × Z
214 208 213 eleqtrd φ X Z II × t II 𝑡 U × Z
215 df-ov X K U × Z Z = K U × Z X Z
216 ovres X U Z Z X K U × Z Z = X K Z
217 15 174 216 syl2anc φ X K U × Z Z = X K Z
218 snidg X U X X
219 15 218 syl φ X X
220 ovres X X Z V X K X × V Z = X K Z
221 219 18 220 syl2anc φ X K X × V Z = X K Z
222 217 221 eqtr4d φ X K U × Z Z = X K X × V Z
223 215 222 eqtr3id φ K U × Z X Z = X K X × V Z
224 eqid II × t II 𝑡 X × V = II × t II 𝑡 X × V
225 snex X V
226 225 a1i φ X V
227 txrest II Top II Top X V V II II × t II 𝑡 X × V = II 𝑡 X × t II 𝑡 V
228 181 181 226 12 227 syl22anc φ II × t II 𝑡 X × V = II 𝑡 X × t II 𝑡 V
229 restsn2 II TopOn 0 1 X 0 1 II 𝑡 X = 𝒫 X
230 68 32 229 sylancr φ II 𝑡 X = 𝒫 X
231 pwsn 𝒫 X = X
232 indisconn X Conn
233 231 232 eqeltri 𝒫 X Conn
234 230 233 eqeltrdi φ II 𝑡 X Conn
235 txconn II 𝑡 X Conn II 𝑡 V Conn II 𝑡 X × t II 𝑡 V Conn
236 234 14 235 syl2anc φ II 𝑡 X × t II 𝑡 V Conn
237 228 236 eqeltrd φ II × t II 𝑡 X × V Conn
238 1 2 3 4 5 6 7 cvmlift2lem6 φ X 0 1 K X × 0 1 II × t II 𝑡 X × 0 1 Cn C
239 32 238 mpdan φ K X × 0 1 II × t II 𝑡 X × 0 1 Cn C
240 xpss2 V 0 1 X × V X × 0 1
241 12 34 240 3syl φ X × V X × 0 1
242 32 snssd φ X 0 1
243 xpss1 X 0 1 X × 0 1 0 1 × 0 1
244 242 243 syl φ X × 0 1 0 1 × 0 1
245 23 restuni II × t II Top X × 0 1 0 1 × 0 1 X × 0 1 = II × t II 𝑡 X × 0 1
246 27 244 245 sylancr φ X × 0 1 = II × t II 𝑡 X × 0 1
247 241 246 sseqtrd φ X × V II × t II 𝑡 X × 0 1
248 eqid II × t II 𝑡 X × 0 1 = II × t II 𝑡 X × 0 1
249 248 cnrest K X × 0 1 II × t II 𝑡 X × 0 1 Cn C X × V II × t II 𝑡 X × 0 1 K X × 0 1 X × V II × t II 𝑡 X × 0 1 𝑡 X × V Cn C
250 239 247 249 syl2anc φ K X × 0 1 X × V II × t II 𝑡 X × 0 1 𝑡 X × V Cn C
251 241 resabs1d φ K X × 0 1 X × V = K X × V
252 225 97 xpex X × 0 1 V
253 252 a1i φ X × 0 1 V
254 restabs II × t II Top X × V X × 0 1 X × 0 1 V II × t II 𝑡 X × 0 1 𝑡 X × V = II × t II 𝑡 X × V
255 28 241 253 254 syl3anc φ II × t II 𝑡 X × 0 1 𝑡 X × V = II × t II 𝑡 X × V
256 255 oveq1d φ II × t II 𝑡 X × 0 1 𝑡 X × V Cn C = II × t II 𝑡 X × V Cn C
257 250 251 256 3eltr3d φ K X × V II × t II 𝑡 X × V Cn C
258 df-ima K X × V = ran K X × V
259 15 snssd φ X U
260 xpss1 X U X × V U × V
261 imass2 X × V U × V K X × V K U × V
262 259 260 261 3syl φ K X × V K U × V
263 262 127 sstrd φ K X × V F -1 M
264 258 263 eqsstrrid φ ran K X × V F -1 M
265 cnrest2 C TopOn B ran K X × V F -1 M F -1 M B K X × V II × t II 𝑡 X × V Cn C K X × V II × t II 𝑡 X × V Cn C 𝑡 F -1 M
266 196 264 138 265 syl3anc φ K X × V II × t II 𝑡 X × V Cn C K X × V II × t II 𝑡 X × V Cn C 𝑡 F -1 M
267 257 266 mpbid φ K X × V II × t II 𝑡 X × V Cn C 𝑡 F -1 M
268 opelxpi X X Y V X Y X × V
269 219 16 268 syl2anc φ X Y X × V
270 259 260 syl φ X × V U × V
271 270 55 sstrd φ X × V 0 1 × 0 1
272 23 restuni II × t II Top X × V 0 1 × 0 1 X × V = II × t II 𝑡 X × V
273 27 271 272 sylancr φ X × V = II × t II 𝑡 X × V
274 269 273 eleqtrd φ X Y II × t II 𝑡 X × V
275 df-ov X K X × V Y = K X × V X Y
276 ovres X X Y V X K X × V Y = X K Y
277 219 16 276 syl2anc φ X K X × V Y = X K Y
278 275 277 eqtr3id φ K X × V X Y = X K Y
279 50 simprd φ X K Y W
280 278 279 eqeltrd φ K X × V X Y W
281 224 237 267 158 161 274 280 conncn φ K X × V : II × t II 𝑡 X × V W
282 273 feq2d φ K X × V : X × V W K X × V : II × t II 𝑡 X × V W
283 281 282 mpbird φ K X × V : X × V W
284 283 219 18 fovrnd φ X K X × V Z W
285 223 284 eqeltrd φ K U × Z X Z W
286 180 195 206 158 161 214 285 conncn φ K U × Z : II × t II 𝑡 U × Z W
287 213 feq2d φ K U × Z : U × Z W K U × Z : II × t II 𝑡 U × Z W
288 286 287 mpbird φ K U × Z : U × Z W
289 288 adantr φ m U n V K U × Z : U × Z W
290 289 110 175 fovrnd φ m U n V m K U × Z Z W
291 179 290 eqeltrd φ m U n V K m × V m Z W
292 61 80 142 159 162 169 291 conncn φ m U n V K m × V : II × t II 𝑡 m × V W
293 168 feq2d φ m U n V K m × V : m × V W K m × V : II × t II 𝑡 m × V W
294 292 293 mpbird φ m U n V K m × V : m × V W
295 294 57 58 fovrnd φ m U n V m K m × V n W
296 60 295 eqeltrrd φ m U n V m K n W
297 296 ralrimivva φ m U n V m K n W
298 funimassov Fun K U × V dom K K U × V W m U n V m K n W
299 122 124 298 syl2anc φ K U × V W m U n V m K n W
300 297 299 mpbird φ K U × V W
301 1 23 8 2 24 26 28 38 10 53 55 300 cvmlift2lem9a φ K U × V II × t II 𝑡 U × V Cn C