Definition df-cms

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

	Ref	Expression
Assertion	df-cms	⊢ CMetSp = { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccms	⊢ CMetSp
1		vw	⊢ 𝑤
2		cms	⊢ MetSp
3		cbs	⊢ Base
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( Base ‘ 𝑤 )
6		vb	⊢ 𝑏
7		cds	⊢ dist
8	4 7	cfv	⊢ ( dist ‘ 𝑤 )
9	6	cv	⊢ 𝑏
10	9 9	cxp	⊢ ( 𝑏 × 𝑏 )
11	8 10	cres	⊢ ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) )
12		ccmet	⊢ CMet
13	9 12	cfv	⊢ ( CMet ‘ 𝑏 )
14	11 13	wcel	⊢ ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 )
15	14 6 5	wsbc	⊢ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 )
16	15 1 2	crab	⊢ { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }
17	0 16	wceq	⊢ CMetSp = { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }