Step | Hyp | Ref
| Expression |
1 | | cmetmet 24653 |
. . 3
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
2 | | metsscmetcld.j |
. . . 4
β’ π½ = (MetOpenβπ·) |
3 | 2 | metsscmetcld 24682 |
. . 3
β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β (Clsdβπ½)) |
4 | 1, 3 | sylan 581 |
. 2
β’ ((π· β (CMetβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β (Clsdβπ½)) |
5 | 1 | adantr 482 |
. . . 4
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β π· β (Metβπ)) |
6 | | eqid 2737 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
7 | 6 | cldss 22383 |
. . . . . 6
β’ (π β (Clsdβπ½) β π β βͺ π½) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β π β βͺ π½) |
9 | | metxmet 23690 |
. . . . . 6
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
10 | 2 | mopnuni 23797 |
. . . . . 6
β’ (π· β (βMetβπ) β π = βͺ π½) |
11 | 5, 9, 10 | 3syl 18 |
. . . . 5
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β π = βͺ π½) |
12 | 8, 11 | sseqtrrd 3986 |
. . . 4
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β π β π) |
13 | | metres2 23719 |
. . . 4
β’ ((π· β (Metβπ) β§ π β π) β (π· βΎ (π Γ π)) β (Metβπ)) |
14 | 5, 12, 13 | syl2anc 585 |
. . 3
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β (π· βΎ (π Γ π)) β (Metβπ)) |
15 | 1, 9 | syl 17 |
. . . . . . . . . 10
β’ (π· β (CMetβπ) β π· β (βMetβπ)) |
16 | 15 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π· β (βMetβπ)) |
17 | 12 | adantr 482 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β π) |
18 | | eqid 2737 |
. . . . . . . . . 10
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
19 | | eqid 2737 |
. . . . . . . . . 10
β’
(MetOpenβ(π·
βΎ (π Γ π))) = (MetOpenβ(π· βΎ (π Γ π))) |
20 | 18, 2, 19 | metrest 23883 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
21 | 16, 17, 20 | syl2anc 585 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
22 | 21 | eqcomd 2743 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (MetOpenβ(π· βΎ (π Γ π))) = (π½ βΎt π)) |
23 | | metxmet 23690 |
. . . . . . . . . . 11
β’ ((π· βΎ (π Γ π)) β (Metβπ) β (π· βΎ (π Γ π)) β (βMetβπ)) |
24 | 14, 23 | syl 17 |
. . . . . . . . . 10
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β (π· βΎ (π Γ π)) β (βMetβπ)) |
25 | | cfilfil 24634 |
. . . . . . . . . 10
β’ (((π· βΎ (π Γ π)) β (βMetβπ) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (Filβπ)) |
26 | 24, 25 | sylan 581 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (Filβπ)) |
27 | | elfvdm 6880 |
. . . . . . . . . 10
β’ (π· β (CMetβπ) β π β dom CMet) |
28 | 27 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β dom CMet) |
29 | | trfg 23245 |
. . . . . . . . 9
β’ ((π β (Filβπ) β§ π β π β§ π β dom CMet) β ((πfilGenπ) βΎt π) = π) |
30 | 26, 17, 28, 29 | syl3anc 1372 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((πfilGenπ) βΎt π) = π) |
31 | 30 | eqcomd 2743 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π = ((πfilGenπ) βΎt π)) |
32 | 22, 31 | oveq12d 7376 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((MetOpenβ(π· βΎ (π Γ π))) fLim π) = ((π½ βΎt π) fLim ((πfilGenπ) βΎt π))) |
33 | 2 | mopntopon 23795 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
34 | 16, 33 | syl 17 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π½ β (TopOnβπ)) |
35 | | filfbas 23202 |
. . . . . . . . . 10
β’ (π β (Filβπ) β π β (fBasβπ)) |
36 | 26, 35 | syl 17 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (fBasβπ)) |
37 | | filsspw 23205 |
. . . . . . . . . . 11
β’ (π β (Filβπ) β π β π« π) |
38 | 26, 37 | syl 17 |
. . . . . . . . . 10
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β π« π) |
39 | 17 | sspwd 4574 |
. . . . . . . . . 10
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π« π β π« π) |
40 | 38, 39 | sstrd 3955 |
. . . . . . . . 9
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β π« π) |
41 | | fbasweak 23219 |
. . . . . . . . 9
β’ ((π β (fBasβπ) β§ π β π« π β§ π β dom CMet) β π β (fBasβπ)) |
42 | 36, 40, 28, 41 | syl3anc 1372 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (fBasβπ)) |
43 | | fgcl 23232 |
. . . . . . . 8
β’ (π β (fBasβπ) β (πfilGenπ) β (Filβπ)) |
44 | 42, 43 | syl 17 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (πfilGenπ) β (Filβπ)) |
45 | | ssfg 23226 |
. . . . . . . . 9
β’ (π β (fBasβπ) β π β (πfilGenπ)) |
46 | 42, 45 | syl 17 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (πfilGenπ)) |
47 | | filtop 23209 |
. . . . . . . . 9
β’ (π β (Filβπ) β π β π) |
48 | 26, 47 | syl 17 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β π) |
49 | 46, 48 | sseldd 3946 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π β (πfilGenπ)) |
50 | | flimrest 23337 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (πfilGenπ) β (Filβπ) β§ π β (πfilGenπ)) β ((π½ βΎt π) fLim ((πfilGenπ) βΎt π)) = ((π½ fLim (πfilGenπ)) β© π)) |
51 | 34, 44, 49, 50 | syl3anc 1372 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((π½ βΎt π) fLim ((πfilGenπ) βΎt π)) = ((π½ fLim (πfilGenπ)) β© π)) |
52 | | flimclsi 23332 |
. . . . . . . . 9
β’ (π β (πfilGenπ) β (π½ fLim (πfilGenπ)) β ((clsβπ½)βπ)) |
53 | 49, 52 | syl 17 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (π½ fLim (πfilGenπ)) β ((clsβπ½)βπ)) |
54 | | cldcls 22396 |
. . . . . . . . 9
β’ (π β (Clsdβπ½) β ((clsβπ½)βπ) = π) |
55 | 54 | ad2antlr 726 |
. . . . . . . 8
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((clsβπ½)βπ) = π) |
56 | 53, 55 | sseqtrd 3985 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (π½ fLim (πfilGenπ)) β π) |
57 | | df-ss 3928 |
. . . . . . 7
β’ ((π½ fLim (πfilGenπ)) β π β ((π½ fLim (πfilGenπ)) β© π) = (π½ fLim (πfilGenπ))) |
58 | 56, 57 | sylib 217 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((π½ fLim (πfilGenπ)) β© π) = (π½ fLim (πfilGenπ))) |
59 | 32, 51, 58 | 3eqtrd 2781 |
. . . . 5
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((MetOpenβ(π· βΎ (π Γ π))) fLim π) = (π½ fLim (πfilGenπ))) |
60 | | simpll 766 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β π· β (CMetβπ)) |
61 | 5, 9 | syl 17 |
. . . . . . 7
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β π· β (βMetβπ)) |
62 | | cfilresi 24662 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (πfilGenπ) β (CauFilβπ·)) |
63 | 61, 62 | sylan 581 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (πfilGenπ) β (CauFilβπ·)) |
64 | 2 | cmetcvg 24652 |
. . . . . 6
β’ ((π· β (CMetβπ) β§ (πfilGenπ) β (CauFilβπ·)) β (π½ fLim (πfilGenπ)) β β
) |
65 | 60, 63, 64 | syl2anc 585 |
. . . . 5
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β (π½ fLim (πfilGenπ)) β β
) |
66 | 59, 65 | eqnetrd 3012 |
. . . 4
β’ (((π· β (CMetβπ) β§ π β (Clsdβπ½)) β§ π β (CauFilβ(π· βΎ (π Γ π)))) β ((MetOpenβ(π· βΎ (π Γ π))) fLim π) β β
) |
67 | 66 | ralrimiva 3144 |
. . 3
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β βπ β (CauFilβ(π· βΎ (π Γ π)))((MetOpenβ(π· βΎ (π Γ π))) fLim π) β β
) |
68 | 19 | iscmet 24651 |
. . 3
β’ ((π· βΎ (π Γ π)) β (CMetβπ) β ((π· βΎ (π Γ π)) β (Metβπ) β§ βπ β (CauFilβ(π· βΎ (π Γ π)))((MetOpenβ(π· βΎ (π Γ π))) fLim π) β β
)) |
69 | 14, 67, 68 | sylanbrc 584 |
. 2
β’ ((π· β (CMetβπ) β§ π β (Clsdβπ½)) β (π· βΎ (π Γ π)) β (CMetβπ)) |
70 | 4, 69 | impbida 800 |
1
β’ (π· β (CMetβπ) β ((π· βΎ (π Γ π)) β (CMetβπ) β π β (Clsdβπ½))) |