Theorem mstps

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

	Ref	Expression
Assertion	mstps	$$⊢M\in \mathrm{MetSp}\to M\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		msxms	$$⊢M\in \mathrm{MetSp}\to M\in \mathrm{\infty MetSp}$$
2		xmstps	$$⊢M\in \mathrm{\infty MetSp}\to M\in \mathrm{TopSp}$$
3	1 2	syl	$$⊢M\in \mathrm{MetSp}\to M\in \mathrm{TopSp}$$