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

Definition df-tms 20032
Description: Define the function mapping a metric to a metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
df-tms  |- toMetSp  =  ( d  e.  U. ran  *Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )

Detailed syntax breakdown of Definition df-tms
StepHypRef Expression
1 ctmt 20029 . 2  class toMetSp
2 vd . . 3  setvar  d
3 cxmt 17929 . . . . 5  class  *Met
43crn 4952 . . . 4  class  ran  *Met
54cuni 4202 . . 3  class  U. ran  *Met
6 cnx 14292 . . . . . . 7  class  ndx
7 cbs 14295 . . . . . . 7  class  Base
86, 7cfv 5529 . . . . . 6  class  ( Base `  ndx )
92cv 1369 . . . . . . . 8  class  d
109cdm 4951 . . . . . . 7  class  dom  d
1110cdm 4951 . . . . . 6  class  dom  dom  d
128, 11cop 3994 . . . . 5  class  <. ( Base `  ndx ) ,  dom  dom  d >.
13 cds 14369 . . . . . . 7  class  dist
146, 13cfv 5529 . . . . . 6  class  ( dist `  ndx )
1514, 9cop 3994 . . . . 5  class  <. ( dist `  ndx ) ,  d >.
1612, 15cpr 3990 . . . 4  class  { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. }
17 cts 14366 . . . . . 6  class TopSet
186, 17cfv 5529 . . . . 5  class  (TopSet `  ndx )
19 cmopn 17934 . . . . . 6  class  MetOpen
209, 19cfv 5529 . . . . 5  class  ( MetOpen `  d )
2118, 20cop 3994 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  d ) >.
22 csts 14293 . . . 4  class sSet
2316, 21, 22co 6203 . . 3  class  ( {
<. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. )
242, 5, 23cmpt 4461 . 2  class  ( d  e.  U. ran  *Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
251, 24wceq 1370 1  wff toMetSp  =  ( d  e.  U. ran  *Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
Colors of variables: wff setvar class
This definition is referenced by:  tmsval  20191
  Copyright terms: Public domain W3C validator