This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metdmdm

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

		Ref	Expression
	Assertion	metdmdm	$⊢ D \in Met (X) \to X = dom dom D$

Step	Hyp	Ref	Expression
1		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
2		xmetdmdm	$⊢ D \in ∞Met (X) \to X = dom dom D$
3	1 2	syl	$⊢ D \in Met (X) \to X = dom dom D$