Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cms Structured version   Visualization version   GIF version

Definition df-cms 23930
 Description: Define the class of 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
StepHypRef Expression
1 ccms 23927 . 2 class CMetSp
2 vw . . . . . . . 8 setvar 𝑤
32cv 1529 . . . . . . 7 class 𝑤
4 cds 16566 . . . . . . 7 class dist
53, 4cfv 6348 . . . . . 6 class (dist‘𝑤)
6 vb . . . . . . . 8 setvar 𝑏
76cv 1529 . . . . . . 7 class 𝑏
87, 7cxp 5546 . . . . . 6 class (𝑏 × 𝑏)
95, 8cres 5550 . . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10 ccmet 23849 . . . . . 6 class CMet
117, 10cfv 6348 . . . . 5 class (CMet‘𝑏)
129, 11wcel 2107 . . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13 cbs 16475 . . . . 5 class Base
143, 13cfv 6348 . . . 4 class (Base‘𝑤)
1512, 6, 14wsbc 3770 . . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16 cms 22920 . . 3 class MetSp
1715, 2, 16crab 3140 . 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
181, 17wceq 1530 1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
 Colors of variables: wff setvar class This definition is referenced by:  iscms  23940
 Copyright terms: Public domain W3C validator