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

Definition df-xms 17885
Description: Define the (proper) class of all extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
df-xms  |-  * MetSp  =  { f  e.  TopSp  |  ( TopOpen `  f )  =  ( MetOpen `  (
( dist `  f )  |`  ( ( Base `  f
)  X.  ( Base `  f ) ) ) ) }

Detailed syntax breakdown of Definition df-xms
StepHypRef Expression
1 cxme 17882 . 2  class  * MetSp
2 vf . . . . . 6  set  f
32cv 1622 . . . . 5  class  f
4 ctopn 13326 . . . . 5  class  TopOpen
53, 4cfv 5255 . . . 4  class  ( TopOpen `  f )
6 cds 13217 . . . . . . 7  class  dist
73, 6cfv 5255 . . . . . 6  class  ( dist `  f )
8 cbs 13148 . . . . . . . 8  class  Base
93, 8cfv 5255 . . . . . . 7  class  ( Base `  f )
109, 9cxp 4687 . . . . . 6  class  ( (
Base `  f )  X.  ( Base `  f
) )
117, 10cres 4691 . . . . 5  class  ( (
dist `  f )  |`  ( ( Base `  f
)  X.  ( Base `  f ) ) )
12 cmopn 16372 . . . . 5  class  MetOpen
1311, 12cfv 5255 . . . 4  class  ( MetOpen `  ( ( dist `  f
)  |`  ( ( Base `  f )  X.  ( Base `  f ) ) ) )
145, 13wceq 1623 . . 3  wff  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) )
15 ctps 16634 . . 3  class  TopSp
1614, 2, 15crab 2547 . 2  class  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
171, 16wceq 1623 1  wff  * MetSp  =  { f  e.  TopSp  |  ( TopOpen `  f )  =  ( MetOpen `  (
( dist `  f )  |`  ( ( Base `  f
)  X.  ( Base `  f ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isxms  17993
  Copyright terms: Public domain W3C validator