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

Metamath Proof Explorer

Theorem xmetdmdm

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

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

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