Theorem metdmdm

Description: Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	metdmdm	$$⊢D\in \mathrm{Met}\left(X\right)\to X=\mathrm{dom}\mathrm{dom}D$$

Proof

Step	Hyp	Ref	Expression
1		metxmet	$$⊢D\in \mathrm{Met}\left(X\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
2		xmetdmdm	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X=\mathrm{dom}\mathrm{dom}D$$
3	1 2	syl	$$⊢D\in \mathrm{Met}\left(X\right)\to X=\mathrm{dom}\mathrm{dom}D$$