Theorem metf

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

	Ref	Expression
Assertion	metf	$$⊢D\in \mathrm{Met}\left(X\right)\to D:X\times X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		metflem	$$⊢D\in \mathrm{Met}\left(X\right)\to \left(D:X\times X⟶ℝ\wedge \forall x\in X\forall y\in X\left(\left(xDy=0\leftrightarrow x=y\right)\wedge \forall z\in XxDy\le \left(zDx\right)+\left(zDy\right)\right)\right)$$
2	1	simpld	$$⊢D\in \mathrm{Met}\left(X\right)\to D:X\times X⟶ℝ$$