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	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
	isms.x	$$⊢X={\mathrm{Base}}_K$$
	isms.d	$$⊢D={\mathrm{dist}\left(K\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	xmstopn	$$⊢K\in \mathrm{\infty MetSp}\to J=\mathrm{MetOpen}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		isms.j	$$⊢J=\mathrm{TopOpen}\left(K\right)$$
2		isms.x	$$⊢X={\mathrm{Base}}_K$$
3		isms.d	$$⊢D={\mathrm{dist}\left(K\right)\upharpoonright }_{\left(X\times X\right)}$$
4	1 2 3	isxms	$$⊢K\in \mathrm{\infty MetSp}\leftrightarrow \left(K\in \mathrm{TopSp}\wedge J=\mathrm{MetOpen}\left(D\right)\right)$$
5	4	simprbi	$$⊢K\in \mathrm{\infty MetSp}\to J=\mathrm{MetOpen}\left(D\right)$$