Metamath Proof Explorer

Theorem ismeti

Description: Properties that determine a metric. (Contributed by NM, 17-Nov-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses ismeti.0 ⊢ X ∈ V
ismeti.1 ⊢ D : X × X ⟶ ℝ
ismeti.2 ⊢ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y
ismeti.3 ⊢ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + z D y
Assertion ismeti ⊢ D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 ismeti.0 ⊢ X ∈ V
2 ismeti.1 ⊢ D : X × X ⟶ ℝ
3 ismeti.2 ⊢ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y
4 ismeti.3 ⊢ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + z D y
5 4 3expa ⊢ x ∈ X ∧ y ∈ X ∧ z ∈ X → x D y ≤ z D x + z D y
6 5 ralrimiva ⊢ x ∈ X ∧ y ∈ X → ∀ z ∈ X x D y ≤ z D x + z D y
7 3 6 jca ⊢ x ∈ X ∧ y ∈ X → x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
8 7 rgen2 ⊢ ∀ x ∈ X ∀ y ∈ X x D y = 0 ↔ x = y ∧ ∀ z ∈ X x D y ≤ z D x + z D y
9 ismet ⊢ X ∈ V → 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
10 1 9 ax-mp ⊢ 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
11 2 8 10 mpbir2an ⊢ D ∈ Met ⁡ X