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 ⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
setsms.d ⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
setsms.k ⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
setsms.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
Assertion setsmstopn ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 setsms.x ⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
2 setsms.d ⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
3 setsms.k ⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
4 setsms.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
5 1 2 3 4 setsmstset ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopSet ‘ 𝐾 ) )
6 df-mopn ⊢ MetOpen = ( 𝑥 ∈ ∪ ran ∞Met ↦ ( topGen ‘ ran ( ball ‘ 𝑥 ) ) )
7 6 dmmptss ⊢ dom MetOpen ⊆ ∪ ran ∞Met
8 7 sseli ⊢ ( 𝐷 ∈ dom MetOpen → 𝐷 ∈ ∪ ran ∞Met )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → 𝐷 ∈ ∪ ran ∞Met )
10 xmetunirn ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
11 9 10 sylib ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
12 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
13 12 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 = ∪ ( MetOpen ‘ 𝐷 ) )
15 2 dmeqd ⊢ ( 𝜑 → dom 𝐷 = dom ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
16 dmres ⊢ dom ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) )
17 15 16 eqtrdi ⊢ ( 𝜑 → dom 𝐷 = ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) ) )
18 inss1 ⊢ ( ( 𝑋 × 𝑋 ) ∩ dom ( dist ‘ 𝑀 ) ) ⊆ ( 𝑋 × 𝑋 )
19 17 18 eqsstrdi ⊢ ( 𝜑 → dom 𝐷 ⊆ ( 𝑋 × 𝑋 ) )
20 dmss ⊢ ( dom 𝐷 ⊆ ( 𝑋 × 𝑋 ) → dom dom 𝐷 ⊆ dom ( 𝑋 × 𝑋 ) )
21 19 20 syl ⊢ ( 𝜑 → dom dom 𝐷 ⊆ dom ( 𝑋 × 𝑋 ) )
22 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
23 21 22 sseqtrdi ⊢ ( 𝜑 → dom dom 𝐷 ⊆ 𝑋 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → dom dom 𝐷 ⊆ 𝑋 )
25 14 24 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → ∪ ( MetOpen ‘ 𝐷 ) ⊆ 𝑋 )
26 sspwuni ⊢ ( ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ↔ ∪ ( MetOpen ‘ 𝐷 ) ⊆ 𝑋 )
27 25 26 sylibr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ∪ ran ∞Met ) → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
28 27 ex ⊢ ( 𝜑 → ( 𝐷 ∈ ∪ ran ∞Met → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ) )
29 8 28 syl5 ⊢ ( 𝜑 → ( 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 ) )
30 ndmfv ⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) = ∅ )
31 0ss ⊢ ∅ ⊆ 𝒫 𝑋
32 30 31 eqsstrdi ⊢ ( ¬ 𝐷 ∈ dom MetOpen → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
33 29 32 pm2.61d1 ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
34 1 2 3 setsmsbas ⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝐾 ) )
35 34 pweqd ⊢ ( 𝜑 → 𝒫 𝑋 = 𝒫 ( Base ‘ 𝐾 ) )
36 33 5 35 3sstr3d ⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
37 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
38 eqid ⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
39 37 38 topnid ⊢ ( ( TopSet ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
40 36 39 syl ⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
41 5 40 eqtrd ⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )