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 25096
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 25093 . 2 class CMetSp
2 vw . . . . . . . 8 setvar 𝑤
32cv 1539 . . . . . . 7 class 𝑤
4 cds 17213 . . . . . . 7 class dist
53, 4cfv 6543 . . . . . 6 class (dist‘𝑤)
6 vb . . . . . . . 8 setvar 𝑏
76cv 1539 . . . . . . 7 class 𝑏
87, 7cxp 5674 . . . . . 6 class (𝑏 × 𝑏)
95, 8cres 5678 . . . . 5 class ((dist‘𝑤) ↾ (𝑏 × 𝑏))
10 ccmet 25015 . . . . . 6 class CMet
117, 10cfv 6543 . . . . 5 class (CMet‘𝑏)
129, 11wcel 2105 . . . 4 wff ((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
13 cbs 17151 . . . . 5 class Base
143, 13cfv 6543 . . . 4 class (Base‘𝑤)
1512, 6, 14wsbc 3777 . . 3 wff [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)
16 cms 24057 . . 3 class MetSp
1715, 2, 16crab 3431 . 2 class {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
181, 17wceq 1540 1 wff CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
Colors of variables: wff setvar class
This definition is referenced by:  iscms  25106
  Copyright terms: Public domain W3C validator