Metamath Proof Explorer


Theorem cnextcn

Description: Extension by continuity. Theorem 1 of BourbakiTop1 p. I.57. Given a topology J on C , a subset A dense in C , this states a condition for F from A to a regular space K to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018)

Ref Expression
Hypotheses cnextf.1 C=J
cnextf.2 B=K
cnextf.3 φJTop
cnextf.4 φKHaus
cnextf.5 φF:AB
cnextf.a φAC
cnextf.6 φclsJA=C
cnextf.7 φxCKfLimfneiJx𝑡AF
cnextcn.8 φKReg
Assertion cnextcn φJCnExtKFJCnK

Proof

Step Hyp Ref Expression
1 cnextf.1 C=J
2 cnextf.2 B=K
3 cnextf.3 φJTop
4 cnextf.4 φKHaus
5 cnextf.5 φF:AB
6 cnextf.a φAC
7 cnextf.6 φclsJA=C
8 cnextf.7 φxCKfLimfneiJx𝑡AF
9 cnextcn.8 φKReg
10 simpll φxCwneiKJCnExtKFxφ
11 simpll φxCwneiKJCnExtKFxdneiJxclsKFdAwφ
12 simpr3 φxCwneiKJCnExtKFxdneiJxclsKFdAwclsKFdAw
13 3 ad2antrr φxCwneiKJCnExtKFxdneiJxclsKFdAwJTop
14 simpr2 φxCwneiKJCnExtKFxdneiJxclsKFdAwdneiJx
15 neii2 JTopdneiJxvJxvvd
16 13 14 15 syl2anc φxCwneiKJCnExtKFxdneiJxclsKFdAwvJxvvd
17 vex xV
18 17 snss xvxv
19 18 biimpri xvxv
20 19 anim1i xvvdxvvd
21 20 anim2i vJxvvdvJxvvd
22 21 anim2i φvJxvvdφvJxvvd
23 22 ex φvJxvvdφvJxvvd
24 3anass φvJxvφvJxv
25 24 anbi1i φvJxvvdφvJxvvd
26 anass φvJxvvdφvJxvvd
27 anass vJxvvdvJxvvd
28 27 anbi2i φvJxvvdφvJxvvd
29 25 26 28 3bitri φvJxvvdφvJxvvd
30 opnneip JTopvJxvvneiJx
31 3 30 syl3an1 φvJxvvneiJx
32 31 adantr φvJxvvdvneiJx
33 simpr2 vdφvJxvvJ
34 33 ex vdφvJxvvJ
35 34 imdistanri φvJxvvdvJvd
36 32 35 jca φvJxvvdvneiJxvJvd
37 29 36 sylbir φvJxvvdvneiJxvJvd
38 23 37 syl6 φvJxvvdvneiJxvJvd
39 38 adantr φclsKFdAwvJxvvdvneiJxvJvd
40 haustop KHausKTop
41 4 40 syl φKTop
42 imassrn FdAranF
43 5 frnd φranFB
44 42 43 sstrid φFdAB
45 ssrin vdvAdA
46 imass2 vAdAFvAFdA
47 45 46 syl vdFvAFdA
48 2 clsss KTopFdABFvAFdAclsKFvAclsKFdA
49 41 44 47 48 syl2an3an φvdclsKFvAclsKFdA
50 sstr clsKFvAclsKFdAclsKFdAwclsKFvAw
51 49 50 sylan φvdclsKFdAwclsKFvAw
52 51 an32s φclsKFdAwvdclsKFvAw
53 52 ex φclsKFdAwvdclsKFvAw
54 53 anim2d φclsKFdAwvJvdvJclsKFvAw
55 54 anim2d φclsKFdAwvneiJxvJvdvneiJxvJclsKFvAw
56 39 55 syld φclsKFdAwvJxvvdvneiJxvJclsKFvAw
57 56 reximdv2 φclsKFdAwvJxvvdvneiJxvJclsKFvAw
58 57 imp φclsKFdAwvJxvvdvneiJxvJclsKFvAw
59 11 12 16 58 syl21anc φxCwneiKJCnExtKFxdneiJxclsKFdAwvneiJxvJclsKFvAw
60 59 3anassrs φxCwneiKJCnExtKFxdneiJxclsKFdAwvneiJxvJclsKFvAw
61 simpr φxCwneiKJCnExtKFxuneiJx𝑡AclsKFuwclsKFuw
62 simp-4l φxCwneiKJCnExtKFxuneiJx𝑡AclsKFuwφ
63 simplr φxCwneiKJCnExtKFxuneiJx𝑡AclsKFuwuneiJx𝑡A
64 imaeq2 u=dAFu=FdA
65 64 fveq2d u=dAclsKFu=clsKFdA
66 65 sseq1d u=dAclsKFuwclsKFdAw
67 66 biimpcd clsKFuwu=dAclsKFdAw
68 67 reximdv clsKFuwdneiJxu=dAdneiJxclsKFdAw
69 fvexd φneiJxV
70 1 toptopon JTopJTopOnC
71 3 70 sylib φJTopOnC
72 71 elfvexd φCV
73 72 6 ssexd φAV
74 elrest neiJxVAVuneiJx𝑡AdneiJxu=dA
75 69 73 74 syl2anc φuneiJx𝑡AdneiJxu=dA
76 75 biimpa φuneiJx𝑡AdneiJxu=dA
77 68 76 impel clsKFuwφuneiJx𝑡AdneiJxclsKFdAw
78 61 62 63 77 syl12anc φxCwneiKJCnExtKFxuneiJx𝑡AclsKFuwdneiJxclsKFdAw
79 eleq1w x=yxCyC
80 79 anbi2d x=yφxCφyC
81 sneq x=yx=y
82 81 fveq2d x=yneiJx=neiJy
83 82 oveq1d x=yneiJx𝑡A=neiJy𝑡A
84 83 oveq2d x=yKfLimfneiJx𝑡A=KfLimfneiJy𝑡A
85 84 fveq1d x=yKfLimfneiJx𝑡AF=KfLimfneiJy𝑡AF
86 85 neeq1d x=yKfLimfneiJx𝑡AFKfLimfneiJy𝑡AF
87 80 86 imbi12d x=yφxCKfLimfneiJx𝑡AFφyCKfLimfneiJy𝑡AF
88 87 8 chvarvv φyCKfLimfneiJy𝑡AF
89 1 2 3 4 5 6 7 88 cnextfvval φxCJCnExtKFx=KfLimfneiJx𝑡AF
90 fvex KfLimfneiJx𝑡AFV
91 90 uniex KfLimfneiJx𝑡AFV
92 91 snid KfLimfneiJx𝑡AFKfLimfneiJx𝑡AF
93 4 adantr φxCKHaus
94 7 eleq2d φxclsJAxC
95 94 biimpar φxCxclsJA
96 71 adantr φxCJTopOnC
97 6 adantr φxCAC
98 simpr φxCxC
99 trnei JTopOnCACxCxclsJAneiJx𝑡AFilA
100 96 97 98 99 syl3anc φxCxclsJAneiJx𝑡AFilA
101 95 100 mpbid φxCneiJx𝑡AFilA
102 5 adantr φxCF:AB
103 2 hausflf2 KHausneiJx𝑡AFilAF:ABKfLimfneiJx𝑡AFKfLimfneiJx𝑡AF1𝑜
104 93 101 102 8 103 syl31anc φxCKfLimfneiJx𝑡AF1𝑜
105 en1b KfLimfneiJx𝑡AF1𝑜KfLimfneiJx𝑡AF=KfLimfneiJx𝑡AF
106 104 105 sylib φxCKfLimfneiJx𝑡AF=KfLimfneiJx𝑡AF
107 92 106 eleqtrrid φxCKfLimfneiJx𝑡AFKfLimfneiJx𝑡AF
108 89 107 eqeltrd φxCJCnExtKFxKfLimfneiJx𝑡AF
109 2 toptopon KTopKTopOnB
110 41 109 sylib φKTopOnB
111 110 adantr φxCKTopOnB
112 flfnei KTopOnBneiJx𝑡AFilAF:ABJCnExtKFxKfLimfneiJx𝑡AFJCnExtKFxBbneiKJCnExtKFxuneiJx𝑡AFub
113 111 101 102 112 syl3anc φxCJCnExtKFxKfLimfneiJx𝑡AFJCnExtKFxBbneiKJCnExtKFxuneiJx𝑡AFub
114 108 113 mpbid φxCJCnExtKFxBbneiKJCnExtKFxuneiJx𝑡AFub
115 114 simprd φxCbneiKJCnExtKFxuneiJx𝑡AFub
116 115 r19.21bi φxCbneiKJCnExtKFxuneiJx𝑡AFub
117 116 ad4ant13 φxCwneiKJCnExtKFxbneiKJCnExtKFxclsKbwuneiJx𝑡AFub
118 41 ad3antrrr φxCbneiKJCnExtKFxclsKbwKTop
119 simplr φxCbneiKJCnExtKFxclsKbwbneiKJCnExtKFx
120 2 neii1 KTopbneiKJCnExtKFxbB
121 118 119 120 syl2anc φxCbneiKJCnExtKFxclsKbwbB
122 simpr φxCbneiKJCnExtKFxclsKbwclsKbw
123 2 clsss KTopbBFubclsKFuclsKb
124 sstr clsKFuclsKbclsKbwclsKFuw
125 123 124 sylan KTopbBFubclsKbwclsKFuw
126 125 3an1rs KTopbBclsKbwFubclsKFuw
127 126 ex KTopbBclsKbwFubclsKFuw
128 127 reximdv KTopbBclsKbwuneiJx𝑡AFubuneiJx𝑡AclsKFuw
129 118 121 122 128 syl3anc φxCbneiKJCnExtKFxclsKbwuneiJx𝑡AFubuneiJx𝑡AclsKFuw
130 129 adantllr φxCwneiKJCnExtKFxbneiKJCnExtKFxclsKbwuneiJx𝑡AFubuneiJx𝑡AclsKFuw
131 117 130 mpd φxCwneiKJCnExtKFxbneiKJCnExtKFxclsKbwuneiJx𝑡AclsKFuw
132 41 ad2antrr φxCwneiKJCnExtKFxKTop
133 9 ad2antrr φxCwneiKJCnExtKFxKReg
134 133 ad2antrr φxCwneiKJCnExtKFxcKJCnExtKFxccwKReg
135 simplr φxCwneiKJCnExtKFxcKJCnExtKFxccwcK
136 simprl φxCwneiKJCnExtKFxcKJCnExtKFxccwJCnExtKFxc
137 regsep KRegcKJCnExtKFxcbKJCnExtKFxbclsKbc
138 134 135 136 137 syl3anc φxCwneiKJCnExtKFxcKJCnExtKFxccwbKJCnExtKFxbclsKbc
139 sstr clsKbccwclsKbw
140 139 expcom cwclsKbcclsKbw
141 140 anim2d cwJCnExtKFxbclsKbcJCnExtKFxbclsKbw
142 141 reximdv cwbKJCnExtKFxbclsKbcbKJCnExtKFxbclsKbw
143 142 ad2antll φxCwneiKJCnExtKFxcKJCnExtKFxccwbKJCnExtKFxbclsKbcbKJCnExtKFxbclsKbw
144 138 143 mpd φxCwneiKJCnExtKFxcKJCnExtKFxccwbKJCnExtKFxbclsKbw
145 simpr φxCwneiKJCnExtKFxwneiKJCnExtKFx
146 neii2 KTopwneiKJCnExtKFxcKJCnExtKFxccw
147 fvex JCnExtKFxV
148 147 snss JCnExtKFxcJCnExtKFxc
149 148 anbi1i JCnExtKFxccwJCnExtKFxccw
150 149 biimpri JCnExtKFxccwJCnExtKFxccw
151 150 reximi cKJCnExtKFxccwcKJCnExtKFxccw
152 146 151 syl KTopwneiKJCnExtKFxcKJCnExtKFxccw
153 132 145 152 syl2anc φxCwneiKJCnExtKFxcKJCnExtKFxccw
154 144 153 r19.29a φxCwneiKJCnExtKFxbKJCnExtKFxbclsKbw
155 anass bKJCnExtKFxbclsKbwbKJCnExtKFxbclsKbw
156 opnneip KTopbKJCnExtKFxbbneiKJCnExtKFx
157 156 3expib KTopbKJCnExtKFxbbneiKJCnExtKFx
158 157 anim1d KTopbKJCnExtKFxbclsKbwbneiKJCnExtKFxclsKbw
159 155 158 syl5bir KTopbKJCnExtKFxbclsKbwbneiKJCnExtKFxclsKbw
160 159 reximdv2 KTopbKJCnExtKFxbclsKbwbneiKJCnExtKFxclsKbw
161 132 154 160 sylc φxCwneiKJCnExtKFxbneiKJCnExtKFxclsKbw
162 131 161 r19.29a φxCwneiKJCnExtKFxuneiJx𝑡AclsKFuw
163 78 162 r19.29a φxCwneiKJCnExtKFxdneiJxclsKFdAw
164 60 163 r19.29a φxCwneiKJCnExtKFxvneiJxvJclsKFvAw
165 simplr φvJclsKFvAwzvclsKFvAw
166 simpll φvJzvφ
167 3 ad2antrr φvJzvJTop
168 simplr φvJzvvJ
169 1 eltopss JTopvJvC
170 167 168 169 syl2anc φvJzvvC
171 simpr φvJzvzv
172 170 171 sseldd φvJzvzC
173 fvexd φvJzvneiJzV
174 73 ad2antrr φvJzvAV
175 opnneip JTopvJzvvneiJz
176 3 175 syl3an1 φvJzvvneiJz
177 176 3expa φvJzvvneiJz
178 elrestr neiJzVAVvneiJzvAneiJz𝑡A
179 173 174 177 178 syl3anc φvJzvvAneiJz𝑡A
180 1 2 3 4 5 6 7 8 cnextfvval φzCJCnExtKFz=KfLimfneiJz𝑡AF
181 180 adantr φzCvAneiJz𝑡AJCnExtKFz=KfLimfneiJz𝑡AF
182 4 adantr φzCKHaus
183 7 eleq2d φzclsJAzC
184 183 biimpar φzCzclsJA
185 71 adantr φzCJTopOnC
186 6 adantr φzCAC
187 simpr φzCzC
188 trnei JTopOnCACzCzclsJAneiJz𝑡AFilA
189 185 186 187 188 syl3anc φzCzclsJAneiJz𝑡AFilA
190 184 189 mpbid φzCneiJz𝑡AFilA
191 5 adantr φzCF:AB
192 eleq1w x=zxCzC
193 192 anbi2d x=zφxCφzC
194 sneq x=zx=z
195 194 fveq2d x=zneiJx=neiJz
196 195 oveq1d x=zneiJx𝑡A=neiJz𝑡A
197 196 oveq2d x=zKfLimfneiJx𝑡A=KfLimfneiJz𝑡A
198 197 fveq1d x=zKfLimfneiJx𝑡AF=KfLimfneiJz𝑡AF
199 198 neeq1d x=zKfLimfneiJx𝑡AFKfLimfneiJz𝑡AF
200 193 199 imbi12d x=zφxCKfLimfneiJx𝑡AFφzCKfLimfneiJz𝑡AF
201 200 8 chvarvv φzCKfLimfneiJz𝑡AF
202 2 hausflf2 KHausneiJz𝑡AFilAF:ABKfLimfneiJz𝑡AFKfLimfneiJz𝑡AF1𝑜
203 182 190 191 201 202 syl31anc φzCKfLimfneiJz𝑡AF1𝑜
204 en1b KfLimfneiJz𝑡AF1𝑜KfLimfneiJz𝑡AF=KfLimfneiJz𝑡AF
205 203 204 sylib φzCKfLimfneiJz𝑡AF=KfLimfneiJz𝑡AF
206 205 adantr φzCvAneiJz𝑡AKfLimfneiJz𝑡AF=KfLimfneiJz𝑡AF
207 110 adantr φzCKTopOnB
208 flfval KTopOnBneiJz𝑡AFilAF:ABKfLimfneiJz𝑡AF=KfLimBFilMapFneiJz𝑡A
209 207 190 191 208 syl3anc φzCKfLimfneiJz𝑡AF=KfLimBFilMapFneiJz𝑡A
210 209 adantr φzCvAneiJz𝑡AKfLimfneiJz𝑡AF=KfLimBFilMapFneiJz𝑡A
211 4 uniexd φKV
212 211 ad2antrr φzCvAneiJz𝑡AKV
213 2 212 eqeltrid φzCvAneiJz𝑡ABV
214 190 adantr φzCvAneiJz𝑡AneiJz𝑡AFilA
215 filfbas neiJz𝑡AFilAneiJz𝑡AfBasA
216 214 215 syl φzCvAneiJz𝑡AneiJz𝑡AfBasA
217 5 ad2antrr φzCvAneiJz𝑡AF:AB
218 simpr φzCvAneiJz𝑡AvAneiJz𝑡A
219 fgfil neiJz𝑡AFilAAfilGenneiJz𝑡A=neiJz𝑡A
220 190 219 syl φzCAfilGenneiJz𝑡A=neiJz𝑡A
221 220 adantr φzCvAneiJz𝑡AAfilGenneiJz𝑡A=neiJz𝑡A
222 218 221 eleqtrrd φzCvAneiJz𝑡AvAAfilGenneiJz𝑡A
223 eqid AfilGenneiJz𝑡A=AfilGenneiJz𝑡A
224 223 imaelfm BVneiJz𝑡AfBasAF:ABvAAfilGenneiJz𝑡AFvABFilMapFneiJz𝑡A
225 213 216 217 222 224 syl31anc φzCvAneiJz𝑡AFvABFilMapFneiJz𝑡A
226 flimclsi FvABFilMapFneiJz𝑡AKfLimBFilMapFneiJz𝑡AclsKFvA
227 225 226 syl φzCvAneiJz𝑡AKfLimBFilMapFneiJz𝑡AclsKFvA
228 210 227 eqsstrd φzCvAneiJz𝑡AKfLimfneiJz𝑡AFclsKFvA
229 206 228 eqsstrrd φzCvAneiJz𝑡AKfLimfneiJz𝑡AFclsKFvA
230 fvex KfLimfneiJz𝑡AFV
231 230 uniex KfLimfneiJz𝑡AFV
232 231 snss KfLimfneiJz𝑡AFclsKFvAKfLimfneiJz𝑡AFclsKFvA
233 229 232 sylibr φzCvAneiJz𝑡AKfLimfneiJz𝑡AFclsKFvA
234 181 233 eqeltrd φzCvAneiJz𝑡AJCnExtKFzclsKFvA
235 166 172 179 234 syl21anc φvJzvJCnExtKFzclsKFvA
236 235 adantlr φvJclsKFvAwzvJCnExtKFzclsKFvA
237 165 236 sseldd φvJclsKFvAwzvJCnExtKFzw
238 237 ralrimiva φvJclsKFvAwzvJCnExtKFzw
239 238 expl φvJclsKFvAwzvJCnExtKFzw
240 239 reximdv φvneiJxvJclsKFvAwvneiJxzvJCnExtKFzw
241 240 ad2antrr φxCwneiKJCnExtKFxvneiJxvJclsKFvAwvneiJxzvJCnExtKFzw
242 164 241 mpd φxCwneiKJCnExtKFxvneiJxzvJCnExtKFzw
243 1 2 3 4 5 6 7 8 cnextf φJCnExtKF:CB
244 243 ffund φFunJCnExtKF
245 244 adantr φvneiJxFunJCnExtKF
246 1 neii1 JTopvneiJxvC
247 3 246 sylan φvneiJxvC
248 243 fdmd φdomJCnExtKF=C
249 248 adantr φvneiJxdomJCnExtKF=C
250 247 249 sseqtrrd φvneiJxvdomJCnExtKF
251 funimass4 FunJCnExtKFvdomJCnExtKFJCnExtKFvwzvJCnExtKFzw
252 245 250 251 syl2anc φvneiJxJCnExtKFvwzvJCnExtKFzw
253 252 biimprd φvneiJxzvJCnExtKFzwJCnExtKFvw
254 253 reximdva φvneiJxzvJCnExtKFzwvneiJxJCnExtKFvw
255 10 242 254 sylc φxCwneiKJCnExtKFxvneiJxJCnExtKFvw
256 255 ralrimiva φxCwneiKJCnExtKFxvneiJxJCnExtKFvw
257 256 ralrimiva φxCwneiKJCnExtKFxvneiJxJCnExtKFvw
258 1 2 cnnei JTopKTopJCnExtKF:CBJCnExtKFJCnKxCwneiKJCnExtKFxvneiJxJCnExtKFvw
259 3 41 243 258 syl3anc φJCnExtKFJCnKxCwneiKJCnExtKFxvneiJxJCnExtKFvw
260 257 259 mpbird φJCnExtKFJCnK