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