Metamath Proof Explorer


Theorem metf

Description: Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006)

Ref Expression
Assertion metf DMetXD:X×X

Proof

Step Hyp Ref Expression
1 metflem DMetXD:X×XxXyXxDy=0x=yzXxDyzDx+zDy
2 1 simpld DMetXD:X×X