Theorem xmstps

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

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left(M\right)=\mathrm{TopOpen}\left(M\right)$$
2		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
3		eqid	$$⊢{\mathrm{dist}\left(M\right)\upharpoonright }_{\left({\mathrm{Base}}_M\times {\mathrm{Base}}_M\right)}={\mathrm{dist}\left(M\right)\upharpoonright }_{\left({\mathrm{Base}}_M\times {\mathrm{Base}}_M\right)}$$
4	1 2 3	isxms	$$⊢M\in \mathrm{\infty MetSp}\leftrightarrow \left(M\in \mathrm{TopSp}\wedge \mathrm{TopOpen}\left(M\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(M\right)\upharpoonright }_{\left({\mathrm{Base}}_M\times {\mathrm{Base}}_M\right)}\right)\right)$$
5	4	simplbi	$$⊢M\in \mathrm{\infty MetSp}\to M\in \mathrm{TopSp}$$