Theorem tmstopn

Description: The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
	tmstopn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	tmstopn	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J=\mathrm{TopOpen}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
2		tmstopn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}$$
4	3 1	tmslem	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge D=\mathrm{dist}\left(K\right)\wedge \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)\right)$$
5	4	simp3d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{MetOpen}\left(D\right)=\mathrm{TopOpen}\left(K\right)$$
6	2 5	syl5eq	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J=\mathrm{TopOpen}\left(K\right)$$