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 mstopn
Description: The topology component of a 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
mstopn ⊢ ( 𝐾 ∈ MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )
Proof
Step
Hyp
Ref
Expression
1
isms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
2
isms.x ⊢ 𝑋 = ( Base ‘ 𝐾 )
3
isms.d ⊢ 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( 𝑋 × 𝑋 ) )
4
1 2 3
isms2 ⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
5
4
simprbi ⊢ ( 𝐾 ∈ MetSp → 𝐽 = ( MetOpen ‘ 𝐷 ) )