Step | Hyp | Ref
| Expression |
1 | | setsms.x |
. . 3
β’ (π β π = (Baseβπ)) |
2 | | setsms.d |
. . 3
β’ (π β π· = ((distβπ) βΎ (π Γ π))) |
3 | | setsms.k |
. . 3
β’ (π β πΎ = (π sSet β¨(TopSetβndx),
(MetOpenβπ·)β©)) |
4 | | setsms.m |
. . 3
β’ (π β π β π) |
5 | 1, 2, 3, 4 | setsmstset 23855 |
. 2
β’ (π β (MetOpenβπ·) = (TopSetβπΎ)) |
6 | | df-mopn 20815 |
. . . . . . . 8
β’ MetOpen =
(π₯ β βͺ ran βMet β¦ (topGenβran
(ballβπ₯))) |
7 | 6 | dmmptss 6197 |
. . . . . . 7
β’ dom
MetOpen β βͺ ran βMet |
8 | 7 | sseli 3944 |
. . . . . 6
β’ (π· β dom MetOpen β π· β βͺ ran βMet) |
9 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π· β βͺ ran
βMet) β π· β
βͺ ran βMet) |
10 | | xmetunirn 23713 |
. . . . . . . . . . 11
β’ (π· β βͺ ran βMet β π· β (βMetβdom dom π·)) |
11 | 9, 10 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π· β βͺ ran
βMet) β π· β
(βMetβdom dom π·)) |
12 | | eqid 2733 |
. . . . . . . . . . 11
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
13 | 12 | mopnuni 23817 |
. . . . . . . . . 10
β’ (π· β (βMetβdom
dom π·) β dom dom π· = βͺ
(MetOpenβπ·)) |
14 | 11, 13 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π· β βͺ ran
βMet) β dom dom π· = βͺ
(MetOpenβπ·)) |
15 | 2 | dmeqd 5865 |
. . . . . . . . . . . . . 14
β’ (π β dom π· = dom ((distβπ) βΎ (π Γ π))) |
16 | | dmres 5963 |
. . . . . . . . . . . . . 14
β’ dom
((distβπ) βΎ
(π Γ π)) = ((π Γ π) β© dom (distβπ)) |
17 | 15, 16 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π β dom π· = ((π Γ π) β© dom (distβπ))) |
18 | | inss1 4192 |
. . . . . . . . . . . . 13
β’ ((π Γ π) β© dom (distβπ)) β (π Γ π) |
19 | 17, 18 | eqsstrdi 4002 |
. . . . . . . . . . . 12
β’ (π β dom π· β (π Γ π)) |
20 | | dmss 5862 |
. . . . . . . . . . . 12
β’ (dom
π· β (π Γ π) β dom dom π· β dom (π Γ π)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β dom dom π· β dom (π Γ π)) |
22 | | dmxpid 5889 |
. . . . . . . . . . 11
β’ dom
(π Γ π) = π |
23 | 21, 22 | sseqtrdi 3998 |
. . . . . . . . . 10
β’ (π β dom dom π· β π) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π· β βͺ ran
βMet) β dom dom π· β π) |
25 | 14, 24 | eqsstrrd 3987 |
. . . . . . . 8
β’ ((π β§ π· β βͺ ran
βMet) β βͺ (MetOpenβπ·) β π) |
26 | | sspwuni 5064 |
. . . . . . . 8
β’
((MetOpenβπ·)
β π« π β
βͺ (MetOpenβπ·) β π) |
27 | 25, 26 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π· β βͺ ran
βMet) β (MetOpenβπ·) β π« π) |
28 | 27 | ex 414 |
. . . . . 6
β’ (π β (π· β βͺ ran
βMet β (MetOpenβπ·) β π« π)) |
29 | 8, 28 | syl5 34 |
. . . . 5
β’ (π β (π· β dom MetOpen β
(MetOpenβπ·) β
π« π)) |
30 | | ndmfv 6881 |
. . . . . 6
β’ (Β¬
π· β dom MetOpen β
(MetOpenβπ·) =
β
) |
31 | | 0ss 4360 |
. . . . . 6
β’ β
β π« π |
32 | 30, 31 | eqsstrdi 4002 |
. . . . 5
β’ (Β¬
π· β dom MetOpen β
(MetOpenβπ·) β
π« π) |
33 | 29, 32 | pm2.61d1 180 |
. . . 4
β’ (π β (MetOpenβπ·) β π« π) |
34 | 1, 2, 3 | setsmsbas 23851 |
. . . . 5
β’ (π β π = (BaseβπΎ)) |
35 | 34 | pweqd 4581 |
. . . 4
β’ (π β π« π = π« (BaseβπΎ)) |
36 | 33, 5, 35 | 3sstr3d 3994 |
. . 3
β’ (π β (TopSetβπΎ) β π«
(BaseβπΎ)) |
37 | | eqid 2733 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
38 | | eqid 2733 |
. . . 4
β’
(TopSetβπΎ) =
(TopSetβπΎ) |
39 | 37, 38 | topnid 17325 |
. . 3
β’
((TopSetβπΎ)
β π« (BaseβπΎ) β (TopSetβπΎ) = (TopOpenβπΎ)) |
40 | 36, 39 | syl 17 |
. 2
β’ (π β (TopSetβπΎ) = (TopOpenβπΎ)) |
41 | 5, 40 | eqtrd 2773 |
1
β’ (π β (MetOpenβπ·) = (TopOpenβπΎ)) |