Metamath Proof Explorer


Theorem 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 ‘ 𝐷 ) )