Theorem mstopn

Description: The topology component of a 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	mstopn	$$⊢K\in \mathrm{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	isms2	$$⊢K\in \mathrm{MetSp}\leftrightarrow \left(D\in \mathrm{Met}\left(X\right)\wedge J=\mathrm{MetOpen}\left(D\right)\right)$$
5	4	simprbi	$$⊢K\in \mathrm{MetSp}\to J=\mathrm{MetOpen}\left(D\right)$$