Theorem msxms

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

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

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	isms	$$⊢M\in \mathrm{MetSp}\leftrightarrow \left(M\in \mathrm{\infty MetSp}\wedge {\mathrm{dist}\left(M\right)\upharpoonright }_{\left({\mathrm{Base}}_M\times {\mathrm{Base}}_M\right)}\in \mathrm{Met}\left({\mathrm{Base}}_M\right)\right)$$
5	4	simplbi	$$⊢M\in \mathrm{MetSp}\to M\in \mathrm{\infty MetSp}$$