Definition df-cms

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

	Ref	Expression
Assertion	df-cms	|- CMetSp = { w e. MetSp | [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccms	|- CMetSp
1		vw	|- w
2		cms	|- MetSp
3		cbs	|- Base
4	1	cv	|- w
5	4 3	cfv	|- ( Base ` w )
6		vb	|- b
7		cds	|- dist
8	4 7	cfv	|- ( dist ` w )
9	6	cv	|- b
10	9 9	cxp	|- ( b X. b )
11	8 10	cres	|- ( ( dist ` w ) |` ( b X. b ) )
12		ccmet	|- CMet
13	9 12	cfv	|- ( CMet ` b )
14	11 13	wcel	|- ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b )
15	14 6 5	wsbc	|- [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b )
16	15 1 2	crab	|- { w e. MetSp | [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) }
17	0 16	wceq	|- CMetSp = { w e. MetSp | [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) }