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∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy

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∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
3 1 2 syl ⊢D∈Met⁡X→D∈Met⁡X↔D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy
4 3 ibi ⊢D∈Met⁡X→D:X×X⟶ℝ∧∀x∈X∀y∈XxDy=0↔x=y∧∀z∈XxDy≤zDx+zDy