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

Definition df-cms 18773
Description: Define the class of all complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.)
Assertion
Ref Expression
df-cms  |- CMetSp  =  {
w  e.  MetSp  |  [. ( Base `  w )  /  b ]. (
( dist `  w )  |`  ( b  X.  b
) )  e.  (
CMet `  b ) }
Distinct variable group:    w, b

Detailed syntax breakdown of Definition df-cms
StepHypRef Expression
1 ccms 18770 . 2  class CMetSp
2 vw . . . . . . . 8  set  w
32cv 1631 . . . . . . 7  class  w
4 cds 13233 . . . . . . 7  class  dist
53, 4cfv 5271 . . . . . 6  class  ( dist `  w )
6 vb . . . . . . . 8  set  b
76cv 1631 . . . . . . 7  class  b
87, 7cxp 4703 . . . . . 6  class  ( b  X.  b )
95, 8cres 4707 . . . . 5  class  ( (
dist `  w )  |`  ( b  X.  b
) )
10 cms 18696 . . . . . 6  class  CMet
117, 10cfv 5271 . . . . 5  class  ( CMet `  b )
129, 11wcel 1696 . . . 4  wff  ( (
dist `  w )  |`  ( b  X.  b
) )  e.  (
CMet `  b )
13 cbs 13164 . . . . 5  class  Base
143, 13cfv 5271 . . . 4  class  ( Base `  w )
1512, 6, 14wsbc 3004 . . 3  wff  [. ( Base `  w )  / 
b ]. ( ( dist `  w )  |`  (
b  X.  b ) )  e.  ( CMet `  b )
16 cmt 17899 . . 3  class  MetSp
1715, 2, 16crab 2560 . 2  class  { w  e.  MetSp  |  [. ( Base `  w )  / 
b ]. ( ( dist `  w )  |`  (
b  X.  b ) )  e.  ( CMet `  b ) }
181, 17wceq 1632 1  wff CMetSp  =  {
w  e.  MetSp  |  [. ( Base `  w )  /  b ]. (
( dist `  w )  |`  ( b  X.  b
) )  e.  (
CMet `  b ) }
Colors of variables: wff set class
This definition is referenced by:  iscms  18783
  Copyright terms: Public domain W3C validator