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

Metamath Proof Explorer

Theorem psmetf

Description: The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion psmetf ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ *

Proof

Step Hyp Ref Expression
1 elfvex ⊢ D ∈ PsMet ⁡ X → X ∈ V
2 ispsmet ⊢ X ∈ V → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
3 1 2 syl ⊢ D ∈ PsMet ⁡ X → D ∈ PsMet ⁡ X ↔ D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
4 3 ibi ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ * ∧ ∀ a ∈ X a D a = 0 ∧ ∀ b ∈ X ∀ c ∈ X a D b ≤ c D a + 𝑒 c D b
5 4 simpld ⊢ D ∈ PsMet ⁡ X → D : X × X ⟶ ℝ *