Metamath Proof Explorer

Theorem xmetf

Description: Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetf ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ *

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ D ∈ ∞Met ⁡ X → X ∈ dom ⁡ ∞Met
2 isxmet ⊢ X ∈ dom ⁡ ∞Met → D ∈ ∞Met ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
3 1 2 syl ⊢ D ∈ ∞Met ⁡ X → D ∈ ∞Met ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
4 3 ibi ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + 𝑒 z D y
5 4 simpld ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ *