Theorem xmetdmdm

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

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

Proof

Step	Hyp	Ref	Expression
1		xmetf	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to D:X\times X⟶{ℝ}^{*}$$
2	1	fdmd	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{dom}D=X\times X$$
3	2	dmeqd	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{dom}\mathrm{dom}D=\mathrm{dom}\left(X\times X\right)$$
4		dmxpid	$$⊢\mathrm{dom}\left(X\times X\right)=X$$
5	3 4	eqtr2di	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X=\mathrm{dom}\mathrm{dom}D$$