Definition df-cms

Description: Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Assertion	df-cms	$$⊢\mathrm{CMetSp}=\left\{w\in \mathrm{MetSp}|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccms	$$class\mathrm{CMetSp}$$
1		vw	$$setvarw$$
2		cms	$$class\mathrm{MetSp}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class{\mathrm{Base}}_w$$
6		vb	$$setvarb$$
7		cds	$$class\mathrm{dist}$$
8	4 7	cfv	$$class\mathrm{dist}\left(w\right)$$
9	6	cv	$$setvarb$$
10	9 9	cxp	$$class\left(b\times b\right)$$
11	8 10	cres	$$class\left({\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\right)$$
12		ccmet	$$class\mathrm{CMet}$$
13	9 12	cfv	$$class\mathrm{CMet}\left(b\right)$$
14	11 13	wcel	$$wff{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)$$
15	14 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)$$
16	15 1 2	crab	$$class\left\{w\in \mathrm{MetSp}|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\right\}$$
17	0 16	wceq	$$wff\mathrm{CMetSp}=\left\{w\in \mathrm{MetSp}|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\right\}$$