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