Metamath Proof Explorer


Theorem setsmstopn

Description: The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses setsms.x φ X = Base M
setsms.d φ D = dist M X × X
setsms.k φ K = M sSet TopSet ndx MetOpen D
setsms.m φ M V
Assertion setsmstopn φ MetOpen D = TopOpen K

Proof

Step Hyp Ref Expression
1 setsms.x φ X = Base M
2 setsms.d φ D = dist M X × X
3 setsms.k φ K = M sSet TopSet ndx MetOpen D
4 setsms.m φ M V
5 1 2 3 4 setsmstset φ MetOpen D = TopSet K
6 df-mopn MetOpen = x ran ∞Met topGen ran ball x
7 6 dmmptss dom MetOpen ran ∞Met
8 7 sseli D dom MetOpen D ran ∞Met
9 simpr φ D ran ∞Met D ran ∞Met
10 xmetunirn D ran ∞Met D ∞Met dom dom D
11 9 10 sylib φ D ran ∞Met D ∞Met dom dom D
12 eqid MetOpen D = MetOpen D
13 12 mopnuni D ∞Met dom dom D dom dom D = MetOpen D
14 11 13 syl φ D ran ∞Met dom dom D = MetOpen D
15 2 dmeqd φ dom D = dom dist M X × X
16 dmres dom dist M X × X = X × X dom dist M
17 15 16 eqtrdi φ dom D = X × X dom dist M
18 inss1 X × X dom dist M X × X
19 17 18 eqsstrdi φ dom D X × X
20 dmss dom D X × X dom dom D dom X × X
21 19 20 syl φ dom dom D dom X × X
22 dmxpid dom X × X = X
23 21 22 sseqtrdi φ dom dom D X
24 23 adantr φ D ran ∞Met dom dom D X
25 14 24 eqsstrrd φ D ran ∞Met MetOpen D X
26 sspwuni MetOpen D 𝒫 X MetOpen D X
27 25 26 sylibr φ D ran ∞Met MetOpen D 𝒫 X
28 27 ex φ D ran ∞Met MetOpen D 𝒫 X
29 8 28 syl5 φ D dom MetOpen MetOpen D 𝒫 X
30 ndmfv ¬ D dom MetOpen MetOpen D =
31 0ss 𝒫 X
32 30 31 eqsstrdi ¬ D dom MetOpen MetOpen D 𝒫 X
33 29 32 pm2.61d1 φ MetOpen D 𝒫 X
34 1 2 3 setsmsbas φ X = Base K
35 34 pweqd φ 𝒫 X = 𝒫 Base K
36 33 5 35 3sstr3d φ TopSet K 𝒫 Base K
37 eqid Base K = Base K
38 eqid TopSet K = TopSet K
39 37 38 topnid TopSet K 𝒫 Base K TopSet K = TopOpen K
40 36 39 syl φ TopSet K = TopOpen K
41 5 40 eqtrd φ MetOpen D = TopOpen K