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