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

Definition df-xms 17880
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 17877 . 2  class  * MetSp
2 vf . . . . . 6  set  f
32cv 1623 . . . . 5  class  f
4 ctopn 13321 . . . . 5  class  TopOpen
53, 4cfv 5222 . . . 4  class  ( TopOpen `  f )
6 cds 13212 . . . . . . 7  class  dist
73, 6cfv 5222 . . . . . 6  class  ( dist `  f )
8 cbs 13143 . . . . . . . 8  class  Base
93, 8cfv 5222 . . . . . . 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 16367 . . . . 5  class  MetOpen
1311, 12cfv 5222 . . . 4  class  ( MetOpen `  ( ( dist `  f
)  |`  ( ( Base `  f )  X.  ( Base `  f ) ) ) )
145, 13wceq 1624 . . 3  wff  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) )
15 ctps 16629 . . 3  class  TopSp
1614, 2, 15crab 2549 . 2  class  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
171, 16wceq 1624 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  17988
  Copyright terms: Public domain W3C validator