psmetdmdm

Description: Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$

Step	Hyp	Ref	Expression
1		elfvex	$⊢ D \in PsMet (X) \to X \in V$
2		ispsmet	$⊢ X \in V \to (D \in PsMet (X) \leftrightarrow (D : X \times X ⟶ ℝ^{*} \land \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y))))$
3	2	biimpa	$⊢ (X \in V \land D \in PsMet (X)) \to (D : X \times X ⟶ ℝ^{*} \land \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)))$
4	1 3	mpancom	$⊢ D \in PsMet (X) \to (D : X \times X ⟶ ℝ^{*} \land \forall x \in X (x D x = 0 \land \forall y \in X \forall z \in X x D y \leq (z D x) +_{𝑒} (z D y)))$
5	4	simpld	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
6		fdm	$⊢ D : X \times X ⟶ ℝ^{*} \to dom D = X \times X$
7	6	dmeqd	$⊢ D : X \times X ⟶ ℝ^{*} \to dom dom D = dom (X \times X)$
8	5 7	syl	$⊢ D \in PsMet (X) \to dom dom D = dom (X \times X)$
9		dmxpid	$⊢ dom (X \times X) = X$
10	8 9	eqtr2di	$⊢ D \in PsMet (X) \to X = dom dom D$

Metamath Proof Explorer