Definition df-cms 22940

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

Assertion

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

Distinct variable group:   𝑤,𝑏

Detailed syntax breakdown of Definition df-cms

Step	Hyp	Ref	Expression
1		ccms 22937	. 2 class CMetSp
2		vw	. . . . . . . 8 setvar 𝑤
3	2	cv 1474	. . . . . . 7 class 𝑤
4		cds 15777	. . . . . . 7 class dist
5	3, 4	cfv 5804	. . . . . 6 class (dist‘𝑤)
6		vb	. . . . . . . 8 setvar 𝑏
7	6	cv 1474	. . . . . . 7 class 𝑏
8	7, 7	cxp 5036	. . . . . 6 class (𝑏 × 𝑏)
9	5, 8	cres 5040	. . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10		cms 22860	. . . . . 6 class CMet
11	7, 10	cfv 5804	. . . . 5 class (CMet‘𝑏)
12	9, 11	wcel 1977	. . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13		cbs 15695	. . . . 5 class Base
14	3, 13	cfv 5804	. . . 4 class (Base‘𝑤)
15	12, 6, 14	wsbc 3402	. . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16		cmt 21933	. . 3 class MetSp
17	15, 2, 16	crab 2900	. 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
18	1, 17	wceq 1475	1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}

This definition is referenced by:  iscms  22950