Metamath Proof Explorer

Theorem metflem

Description: Lemma for metf and others. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metflem ⊢ 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

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ D ∈ Met ⁡ X → X ∈ dom ⁡ Met
2 ismet ⊢ 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