Metamath Proof Explorer

Theorem psmetdmdm

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

Ref Expression
Assertion psmetdmdm ⊢ D ∈ PsMet ⁡ X → X = dom ⁡ dom ⁡ D

Proof

Step Hyp Ref Expression
1 elfvex ⊢ D ∈ PsMet ⁡ X → X ∈ V
2 ispsmet ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
3 2 biimpa ⊢ X ∈ V ∧ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
4 1 3 mpancom ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ x ∈ X x D x = 0 ∧ ∀ y ∈ X ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
5 4 simpld ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ *
6 fdm ⊢ D : X × X ⟶ ℝ * → dom ⁡ D = X × X
7 6 dmeqd ⊢ D : X × X ⟶ ℝ * → dom ⁡ dom ⁡ D = dom ⁡ X × X
8 5 7 syl ⊢ D ∈ PsMet ⁡ X → dom ⁡ dom ⁡ D = dom ⁡ X × X
9 dmxpid ⊢ dom ⁡ X × X = X
10 8 9 eqtr2di ⊢ D ∈ PsMet ⁡ X → X = dom ⁡ dom ⁡ D