Step | Hyp | Ref
| Expression |
1 | | metxmet 23690 |
. . . . . . 7
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π· β (βMetβπ)) |
3 | | metsscmetcld.j |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
4 | 3 | mopntopon 23795 |
. . . . . 6
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π½ β (TopOnβπ)) |
6 | | resss 5963 |
. . . . . . 7
β’ (π· βΎ (π Γ π)) β π· |
7 | | dmss 5859 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)) β π· β dom (π· βΎ (π Γ π)) β dom π·) |
8 | | dmss 5859 |
. . . . . . 7
β’ (dom
(π· βΎ (π Γ π)) β dom π· β dom dom (π· βΎ (π Γ π)) β dom dom π·) |
9 | 6, 7, 8 | mp2b 10 |
. . . . . 6
β’ dom dom
(π· βΎ (π Γ π)) β dom dom π· |
10 | | cmetmet 24653 |
. . . . . . . 8
β’ ((π· βΎ (π Γ π)) β (CMetβπ) β (π· βΎ (π Γ π)) β (Metβπ)) |
11 | | metdmdm 23692 |
. . . . . . . 8
β’ ((π· βΎ (π Γ π)) β (Metβπ) β π = dom dom (π· βΎ (π Γ π))) |
12 | 10, 11 | syl 17 |
. . . . . . 7
β’ ((π· βΎ (π Γ π)) β (CMetβπ) β π = dom dom (π· βΎ (π Γ π))) |
13 | | metdmdm 23692 |
. . . . . . 7
β’ (π· β (Metβπ) β π = dom dom π·) |
14 | | sseq12 3972 |
. . . . . . 7
β’ ((π = dom dom (π· βΎ (π Γ π)) β§ π = dom dom π·) β (π β π β dom dom (π· βΎ (π Γ π)) β dom dom π·)) |
15 | 12, 13, 14 | syl2anr 598 |
. . . . . 6
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β (π β π β dom dom (π· βΎ (π Γ π)) β dom dom π·)) |
16 | 9, 15 | mpbiri 258 |
. . . . 5
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β π) |
17 | | flimcls 23339 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π) β (π₯ β ((clsβπ½)βπ) β βπ β (Filβπ)(π β π β§ π₯ β (π½ fLim π)))) |
18 | 5, 16, 17 | syl2anc 585 |
. . . 4
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β (π₯ β ((clsβπ½)βπ) β βπ β (Filβπ)(π β π β§ π₯ β (π½ fLim π)))) |
19 | | simprrr 781 |
. . . . . 6
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π₯ β (π½ fLim π)) |
20 | 2 | adantr 482 |
. . . . . . . 8
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π· β (βMetβπ)) |
21 | 3 | methaus 23879 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β Haus) |
22 | | hausflimi 23334 |
. . . . . . . 8
β’ (π½ β Haus β
β*π₯ π₯ β (π½ fLim π)) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . 7
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β β*π₯ π₯ β (π½ fLim π)) |
24 | 20, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π½ β (TopOnβπ)) |
25 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π β (Filβπ)) |
26 | | simprrl 780 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π β π) |
27 | | flimrest 23337 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π β (Filβπ) β§ π β π) β ((π½ βΎt π) fLim (π βΎt π)) = ((π½ fLim π) β© π)) |
28 | 24, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β ((π½ βΎt π) fLim (π βΎt π)) = ((π½ fLim π) β© π)) |
29 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π β π) |
30 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
31 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(MetOpenβ(π·
βΎ (π Γ π))) = (MetOpenβ(π· βΎ (π Γ π))) |
32 | 30, 3, 31 | metrest 23883 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π β π) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
33 | 20, 29, 32 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
34 | 33 | oveq1d 7373 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β ((π½ βΎt π) fLim (π βΎt π)) = ((MetOpenβ(π· βΎ (π Γ π))) fLim (π βΎt π))) |
35 | 28, 34 | eqtr3d 2779 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β ((π½ fLim π) β© π) = ((MetOpenβ(π· βΎ (π Γ π))) fLim (π βΎt π))) |
36 | | simplr 768 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β (π· βΎ (π Γ π)) β (CMetβπ)) |
37 | 3 | flimcfil 24681 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π₯ β (π½ fLim π)) β π β (CauFilβπ·)) |
38 | 20, 19, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π β (CauFilβπ·)) |
39 | | cfilres 24663 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π β (Filβπ) β§ π β π) β (π β (CauFilβπ·) β (π βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) |
40 | 20, 25, 26, 39 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β (π β (CauFilβπ·) β (π βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) |
41 | 38, 40 | mpbid 231 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β (π βΎt π) β (CauFilβ(π· βΎ (π Γ π)))) |
42 | 31 | cmetcvg 24652 |
. . . . . . . . . 10
β’ (((π· βΎ (π Γ π)) β (CMetβπ) β§ (π βΎt π) β (CauFilβ(π· βΎ (π Γ π)))) β ((MetOpenβ(π· βΎ (π Γ π))) fLim (π βΎt π)) β β
) |
43 | 36, 41, 42 | syl2anc 585 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β ((MetOpenβ(π· βΎ (π Γ π))) fLim (π βΎt π)) β β
) |
44 | 35, 43 | eqnetrd 3012 |
. . . . . . . 8
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β ((π½ fLim π) β© π) β β
) |
45 | | ndisj 4328 |
. . . . . . . 8
β’ (((π½ fLim π) β© π) β β
β βπ₯(π₯ β (π½ fLim π) β§ π₯ β π)) |
46 | 44, 45 | sylib 217 |
. . . . . . 7
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β βπ₯(π₯ β (π½ fLim π) β§ π₯ β π)) |
47 | | mopick 2626 |
. . . . . . 7
β’
((β*π₯ π₯ β (π½ fLim π) β§ βπ₯(π₯ β (π½ fLim π) β§ π₯ β π)) β (π₯ β (π½ fLim π) β π₯ β π)) |
48 | 23, 46, 47 | syl2anc 585 |
. . . . . 6
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β (π₯ β (π½ fLim π) β π₯ β π)) |
49 | 19, 48 | mpd 15 |
. . . . 5
β’ (((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β§ (π β (Filβπ) β§ (π β π β§ π₯ β (π½ fLim π)))) β π₯ β π) |
50 | 49 | rexlimdvaa 3154 |
. . . 4
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β (βπ β (Filβπ)(π β π β§ π₯ β (π½ fLim π)) β π₯ β π)) |
51 | 18, 50 | sylbid 239 |
. . 3
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β (π₯ β ((clsβπ½)βπ) β π₯ β π)) |
52 | 51 | ssrdv 3951 |
. 2
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β ((clsβπ½)βπ) β π) |
53 | 3 | mopntop 23796 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Top) |
54 | 2, 53 | syl 17 |
. . 3
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π½ β Top) |
55 | 3 | mopnuni 23797 |
. . . . 5
β’ (π· β (βMetβπ) β π = βͺ π½) |
56 | 2, 55 | syl 17 |
. . . 4
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π = βͺ π½) |
57 | 16, 56 | sseqtrd 3985 |
. . 3
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β βͺ π½) |
58 | | eqid 2737 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
59 | 58 | iscld4 22419 |
. . 3
β’ ((π½ β Top β§ π β βͺ π½)
β (π β
(Clsdβπ½) β
((clsβπ½)βπ) β π)) |
60 | 54, 57, 59 | syl2anc 585 |
. 2
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β (π β (Clsdβπ½) β ((clsβπ½)βπ) β π)) |
61 | 52, 60 | mpbird 257 |
1
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β (Clsdβπ½)) |