Theorem msf

Description: The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)

	Ref	Expression
Hypotheses	msf.x	$$⊢X={\mathrm{Base}}_M$$
	msf.d	$$⊢D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	msf	$$⊢M\in \mathrm{MetSp}\to D:X\times X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		msf.x	$$⊢X={\mathrm{Base}}_M$$
2		msf.d	$$⊢D={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
3	1 2	msmet	$$⊢M\in \mathrm{MetSp}\to D\in \mathrm{Met}\left(X\right)$$
4		metf	$$⊢D\in \mathrm{Met}\left(X\right)\to D:X\times X⟶ℝ$$
5	3 4	syl	$$⊢M\in \mathrm{MetSp}\to D:X\times X⟶ℝ$$