Definition df-ms

Description: Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	df-ms	$$⊢\mathrm{MetSp}=\left\{f\in \mathrm{\infty MetSp}|{\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cms	$$class\mathrm{MetSp}$$
1		vf	$$setvarf$$
2		cxms	$$class\mathrm{\infty MetSp}$$
3		cds	$$class\mathrm{dist}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class\mathrm{dist}\left(f\right)$$
6		cbs	$$class\mathrm{Base}$$
7	4 6	cfv	$$class{\mathrm{Base}}_f$$
8	7 7	cxp	$$class\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)$$
9	5 8	cres	$$class\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)$$
10		cmet	$$class\mathrm{Met}$$
11	7 10	cfv	$$class\mathrm{Met}\left({\mathrm{Base}}_f\right)$$
12	9 11	wcel	$$wff{\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)$$
13	12 1 2	crab	$$class\left\{f\in \mathrm{\infty MetSp}|{\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)\right\}$$
14	0 13	wceq	$$wff\mathrm{MetSp}=\left\{f\in \mathrm{\infty MetSp}|{\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\in \mathrm{Met}\left({\mathrm{Base}}_f\right)\right\}$$