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 23541
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 23538 . 2 class CMetSp
2 vw . . . . . . . 8 setvar 𝑤
32cv 1600 . . . . . . 7 class 𝑤
4 cds 16347 . . . . . . 7 class dist
53, 4cfv 6135 . . . . . 6 class (dist‘𝑤)
6 vb . . . . . . . 8 setvar 𝑏
76cv 1600 . . . . . . 7 class 𝑏
87, 7cxp 5353 . . . . . 6 class (𝑏 × 𝑏)
95, 8cres 5357 . . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10 ccmet 23460 . . . . . 6 class CMet
117, 10cfv 6135 . . . . 5 class (CMet‘𝑏)
129, 11wcel 2106 . . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13 cbs 16255 . . . . 5 class Base
143, 13cfv 6135 . . . 4 class (Base‘𝑤)
1512, 6, 14wsbc 3651 . . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16 cms 22531 . . 3 class MetSp
1715, 2, 16crab 3093 . 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
181, 17wceq 1601 1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
Colors of variables: wff setvar class
This definition is referenced by:  iscms  23551
  Copyright terms: Public domain W3C validator