ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xms Unicode version

Definition df-xms 12403
Description: Define the (proper) class of 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 cxms 12400 . 2  class  *MetSp
2 vf . . . . . 6  setvar  f
32cv 1313 . . . . 5  class  f
4 ctopn 12016 . . . . 5  class  TopOpen
53, 4cfv 5091 . . . 4  class  ( TopOpen `  f )
6 cds 11925 . . . . . . 7  class  dist
73, 6cfv 5091 . . . . . 6  class  ( dist `  f )
8 cbs 11854 . . . . . . . 8  class  Base
93, 8cfv 5091 . . . . . . 7  class  ( Base `  f )
109, 9cxp 4505 . . . . . 6  class  ( (
Base `  f )  X.  ( Base `  f
) )
117, 10cres 4509 . . . . 5  class  ( (
dist `  f )  |`  ( ( Base `  f
)  X.  ( Base `  f ) ) )
12 cmopn 12049 . . . . 5  class  MetOpen
1311, 12cfv 5091 . . . 4  class  ( MetOpen `  ( ( dist `  f
)  |`  ( ( Base `  f )  X.  ( Base `  f ) ) ) )
145, 13wceq 1314 . . 3  wff  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) )
15 ctps 12092 . . 3  class  TopSp
1614, 2, 15crab 2395 . 2  class  { f  e.  TopSp  |  ( TopOpen `  f )  =  (
MetOpen `  ( ( dist `  f )  |`  (
( Base `  f )  X.  ( Base `  f
) ) ) ) }
171, 16wceq 1314 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  12515
  Copyright terms: Public domain W3C validator