Theorem mstps

Description: A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	mstps	⊢ ( 𝑀 ∈ MetSp → 𝑀 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		msxms	⊢ ( 𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp )
2		xmstps	⊢ ( 𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp )
3	1 2	syl	⊢ ( 𝑀 ∈ MetSp → 𝑀 ∈ TopSp )