This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Open sets of a metric space xmstopn
Description: The topology component of an extended metric space coincides with the
topology generated by the metric component. (Contributed by Mario
Carneiro , 26-Aug-2015)
Ref
Expression
Hypotheses
isms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
isms.x ⊢ 𝑋 = ( Base ‘ 𝐾 )
isms.d ⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion
xmstopn ⊢ ( 𝐾 ∈ ∞MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )
Proof
Step
Hyp
Ref
Expression
1
isms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
2
isms.x ⊢ 𝑋 = ( Base ‘ 𝐾 )
3
isms.d ⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
4
1 2 3
isxms ⊢ ( 𝐾 ∈ ∞MetSp ↔ ( 𝐾 ∈ TopSp ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
5
4
simprbi ⊢ ( 𝐾 ∈ ∞MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )