Theorem tmsbas

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

	Ref	Expression
Hypothesis	tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
Assertion	tmsbas	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X={\mathrm{Base}}_K$$

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	$$⊢K=\mathrm{toMetSp}\left(D\right)$$
2		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\}$$
3	2 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)$$
4	3	simp1d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X={\mathrm{Base}}_K$$