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

Definition df-tms 19872
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 19869 . 2  class toMetSp
2 vd . . 3  setvar  d
3 cxmt 17776 . . . . 5  class  *Met
43crn 4836 . . . 4  class  ran  *Met
54cuni 4086 . . 3  class  U. ran  *Met
6 cnx 14163 . . . . . . 7  class  ndx
7 cbs 14166 . . . . . . 7  class  Base
86, 7cfv 5413 . . . . . 6  class  ( Base `  ndx )
92cv 1368 . . . . . . . 8  class  d
109cdm 4835 . . . . . . 7  class  dom  d
1110cdm 4835 . . . . . 6  class  dom  dom  d
128, 11cop 3878 . . . . 5  class  <. ( Base `  ndx ) ,  dom  dom  d >.
13 cds 14239 . . . . . . 7  class  dist
146, 13cfv 5413 . . . . . 6  class  ( dist `  ndx )
1514, 9cop 3878 . . . . 5  class  <. ( dist `  ndx ) ,  d >.
1612, 15cpr 3874 . . . 4  class  { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. }
17 cts 14236 . . . . . 6  class TopSet
186, 17cfv 5413 . . . . 5  class  (TopSet `  ndx )
19 cmopn 17781 . . . . . 6  class  MetOpen
209, 19cfv 5413 . . . . 5  class  ( MetOpen `  d )
2118, 20cop 3878 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  d ) >.
22 csts 14164 . . . 4  class sSet
2316, 21, 22co 6086 . . 3  class  ( {
<. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. )
242, 5, 23cmpt 4345 . 2  class  ( d  e.  U. ran  *Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
251, 24wceq 1369 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  20031
  Copyright terms: Public domain W3C validator