Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2733 |
. 2
β’ βͺ πΎ =
βͺ πΎ |
3 | | cnextucn.v |
. . 3
β’ (π β π β TopSp) |
4 | | cnextucn.j |
. . . 4
β’ π½ = (TopOpenβπ) |
5 | 4 | tpstop 22309 |
. . 3
β’ (π β TopSp β π½ β Top) |
6 | 3, 5 | syl 17 |
. 2
β’ (π β π½ β Top) |
7 | | cnextucn.h |
. 2
β’ (π β πΎ β Haus) |
8 | | cnextucn.f |
. . 3
β’ (π β πΉ:π΄βΆπ) |
9 | | cnextucn.t |
. . . . 5
β’ (π β π β TopSp) |
10 | | cnextucn.y |
. . . . . 6
β’ π = (Baseβπ) |
11 | | cnextucn.k |
. . . . . 6
β’ πΎ = (TopOpenβπ) |
12 | 10, 11 | tpsuni 22308 |
. . . . 5
β’ (π β TopSp β π = βͺ
πΎ) |
13 | 9, 12 | syl 17 |
. . . 4
β’ (π β π = βͺ πΎ) |
14 | 13 | feq3d 6659 |
. . 3
β’ (π β (πΉ:π΄βΆπ β πΉ:π΄βΆβͺ πΎ)) |
15 | 8, 14 | mpbid 231 |
. 2
β’ (π β πΉ:π΄βΆβͺ πΎ) |
16 | | cnextucn.a |
. . 3
β’ (π β π΄ β π) |
17 | | cnextucn.x |
. . . . 5
β’ π = (Baseβπ) |
18 | 17, 4 | tpsuni 22308 |
. . . 4
β’ (π β TopSp β π = βͺ
π½) |
19 | 3, 18 | syl 17 |
. . 3
β’ (π β π = βͺ π½) |
20 | 16, 19 | sseqtrd 3988 |
. 2
β’ (π β π΄ β βͺ π½) |
21 | | cnextucn.c |
. . 3
β’ (π β ((clsβπ½)βπ΄) = π) |
22 | 21, 19 | eqtrd 2773 |
. 2
β’ (π β ((clsβπ½)βπ΄) = βͺ π½) |
23 | 10, 11 | istps 22306 |
. . . . . 6
β’ (π β TopSp β πΎ β (TopOnβπ)) |
24 | 9, 23 | sylib 217 |
. . . . 5
β’ (π β πΎ β (TopOnβπ)) |
25 | 24 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β πΎ β (TopOnβπ)) |
26 | 19 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π₯ β π β π₯ β βͺ π½)) |
27 | 26 | biimpar 479 |
. . . . . 6
β’ ((π β§ π₯ β βͺ π½) β π₯ β π) |
28 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β βͺ π½) β ((clsβπ½)βπ΄) = π) |
29 | 27, 28 | eleqtrrd 2837 |
. . . . 5
β’ ((π β§ π₯ β βͺ π½) β π₯ β ((clsβπ½)βπ΄)) |
30 | | toptopon2 22290 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
31 | 6, 30 | sylib 217 |
. . . . . . . 8
β’ (π β π½ β (TopOnββͺ π½)) |
32 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = βͺ
π½ β (TopOnβπ) = (TopOnββͺ π½)) |
33 | 32 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = βͺ
π½ β (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½))) |
34 | 19, 33 | syl 17 |
. . . . . . . 8
β’ (π β (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½))) |
35 | 31, 34 | mpbird 257 |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
36 | 35 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β βͺ π½) β π½ β (TopOnβπ)) |
37 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β βͺ π½) β π΄ β π) |
38 | | trnei 23266 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ π₯ β π) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
39 | 36, 37, 27, 38 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β βͺ π½) β (π₯ β ((clsβπ½)βπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄))) |
40 | 29, 39 | mpbid 231 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄)) |
41 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β πΉ:π΄βΆπ) |
42 | | flfval 23364 |
. . . 4
β’ ((πΎ β (TopOnβπ) β§ (((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β§ πΉ:π΄βΆπ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = (πΎ fLim ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)))) |
43 | 25, 40, 41, 42 | syl3anc 1372 |
. . 3
β’ ((π β§ π₯ β βͺ π½) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) = (πΎ fLim ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)))) |
44 | | cnextucn.w |
. . . . 5
β’ (π β π β CUnifSp) |
45 | 44 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β π β CUnifSp) |
46 | | cnextucn.l |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (CauFiluβπ)) |
47 | 27, 46 | syldan 592 |
. . . . 5
β’ ((π β§ π₯ β βͺ π½) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (CauFiluβπ)) |
48 | | cnextucn.u |
. . . . . 6
β’ π = (UnifStβπ) |
49 | 48 | fveq2i 6849 |
. . . . 5
β’
(CauFiluβπ) =
(CauFiluβ(UnifStβπ)) |
50 | 47, 49 | eleqtrdi 2844 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β
(CauFiluβ(UnifStβπ))) |
51 | 10 | fvexi 6860 |
. . . . 5
β’ π β V |
52 | | filfbas 23222 |
. . . . . 6
β’
((((neiβπ½)β{π₯}) βΎt π΄) β (Filβπ΄) β (((neiβπ½)β{π₯}) βΎt π΄) β (fBasβπ΄)) |
53 | 40, 52 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β βͺ π½) β (((neiβπ½)β{π₯}) βΎt π΄) β (fBasβπ΄)) |
54 | | fmfil 23318 |
. . . . 5
β’ ((π β V β§
(((neiβπ½)β{π₯}) βΎt π΄) β (fBasβπ΄) β§ πΉ:π΄βΆπ) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (Filβπ)) |
55 | 51, 53, 41, 54 | mp3an2i 1467 |
. . . 4
β’ ((π β§ π₯ β βͺ π½) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (Filβπ)) |
56 | 10, 11 | cuspcvg 23676 |
. . . 4
β’ ((π β CUnifSp β§ ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β
(CauFiluβ(UnifStβπ)) β§ ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (Filβπ)) β (πΎ fLim ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄))) β β
) |
57 | 45, 50, 55, 56 | syl3anc 1372 |
. . 3
β’ ((π β§ π₯ β βͺ π½) β (πΎ fLim ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄))) β β
) |
58 | 43, 57 | eqnetrd 3008 |
. 2
β’ ((π β§ π₯ β βͺ π½) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β
) |
59 | | cuspusp 23675 |
. . . 4
β’ (π β CUnifSp β π β UnifSp) |
60 | 44, 59 | syl 17 |
. . 3
β’ (π β π β UnifSp) |
61 | 11 | uspreg 23649 |
. . 3
β’ ((π β UnifSp β§ πΎ β Haus) β πΎ β Reg) |
62 | 60, 7, 61 | syl2anc 585 |
. 2
β’ (π β πΎ β Reg) |
63 | 1, 2, 6, 7, 15, 20, 22, 58, 62 | cnextcn 23441 |
1
β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) |