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

Definition df-cmet 18699
Description: Define the class of complete metrics. (Contributed by Mario Carneiro, 1-May-2014.)
Assertion
Ref Expression
df-cmet  |-  CMet  =  ( x  e.  _V  |->  { d  e.  ( Met `  x )  |  A. f  e.  (CauFil `  d )
( ( MetOpen `  d
)  fLim  f )  =/=  (/) } )
Distinct variable group:    f, d, x

Detailed syntax breakdown of Definition df-cmet
StepHypRef Expression
1 cms 18696 . 2  class  CMet
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 vd . . . . . . . . 9  set  d
54cv 1631 . . . . . . . 8  class  d
6 cmopn 16388 . . . . . . . 8  class  MetOpen
75, 6cfv 5271 . . . . . . 7  class  ( MetOpen `  d )
8 vf . . . . . . . 8  set  f
98cv 1631 . . . . . . 7  class  f
10 cflim 17645 . . . . . . 7  class  fLim
117, 9, 10co 5874 . . . . . 6  class  ( (
MetOpen `  d )  fLim  f )
12 c0 3468 . . . . . 6  class  (/)
1311, 12wne 2459 . . . . 5  wff  ( (
MetOpen `  d )  fLim  f )  =/=  (/)
14 ccfil 18694 . . . . . 6  class CauFil
155, 14cfv 5271 . . . . 5  class  (CauFil `  d )
1613, 8, 15wral 2556 . . . 4  wff  A. f  e.  (CauFil `  d )
( ( MetOpen `  d
)  fLim  f )  =/=  (/)
172cv 1631 . . . . 5  class  x
18 cme 16386 . . . . 5  class  Met
1917, 18cfv 5271 . . . 4  class  ( Met `  x )
2016, 4, 19crab 2560 . . 3  class  { d  e.  ( Met `  x
)  |  A. f  e.  (CauFil `  d )
( ( MetOpen `  d
)  fLim  f )  =/=  (/) }
212, 3, 20cmpt 4093 . 2  class  ( x  e.  _V  |->  { d  e.  ( Met `  x
)  |  A. f  e.  (CauFil `  d )
( ( MetOpen `  d
)  fLim  f )  =/=  (/) } )
221, 21wceq 1632 1  wff  CMet  =  ( x  e.  _V  |->  { d  e.  ( Met `  x )  |  A. f  e.  (CauFil `  d )
( ( MetOpen `  d
)  fLim  f )  =/=  (/) } )
Colors of variables: wff set class
This definition is referenced by:  iscmet  18726
  Copyright terms: Public domain W3C validator