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

Definition df-cms 23113
 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 23110 . 2 class CMetSp
2 vw . . . . . . . 8 setvar 𝑤
32cv 1480 . . . . . . 7 class 𝑤
4 cds 15931 . . . . . . 7 class dist
53, 4cfv 5876 . . . . . 6 class (dist‘𝑤)
6 vb . . . . . . . 8 setvar 𝑏
76cv 1480 . . . . . . 7 class 𝑏
87, 7cxp 5102 . . . . . 6 class (𝑏 × 𝑏)
95, 8cres 5106 . . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10 cms 23033 . . . . . 6 class CMet
117, 10cfv 5876 . . . . 5 class (CMet‘𝑏)
129, 11wcel 1988 . . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13 cbs 15838 . . . . 5 class Base
143, 13cfv 5876 . . . 4 class (Base‘𝑤)
1512, 6, 14wsbc 3429 . . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16 cmt 22104 . . 3 class MetSp
1715, 2, 16crab 2913 . 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
181, 17wceq 1481 1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
 Colors of variables: wff setvar class This definition is referenced by:  iscms  23123
 Copyright terms: Public domain W3C validator