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

Definition df-cms 22853
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
StepHypRef Expression
1 ccms 22850 . 2 class CMetSp
2 vw . . . . . . . 8 setvar 𝑤
32cv 1473 . . . . . . 7 class 𝑤
4 cds 15719 . . . . . . 7 class dist
53, 4cfv 5786 . . . . . 6 class (dist‘𝑤)
6 vb . . . . . . . 8 setvar 𝑏
76cv 1473 . . . . . . 7 class 𝑏
87, 7cxp 5022 . . . . . 6 class (𝑏 × 𝑏)
95, 8cres 5026 . . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10 cms 22774 . . . . . 6 class CMet
117, 10cfv 5786 . . . . 5 class (CMet‘𝑏)
129, 11wcel 1975 . . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13 cbs 15637 . . . . 5 class Base
143, 13cfv 5786 . . . 4 class (Base‘𝑤)
1512, 6, 14wsbc 3397 . . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16 cmt 21870 . . 3 class MetSp
1715, 2, 16crab 2895 . 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
181, 17wceq 1474 1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
Colors of variables: wff setvar class
This definition is referenced by:  iscms  22863
  Copyright terms: Public domain W3C validator