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

Definition df-tms 17903
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 17900 . 2  class toMetSp
2 vd . . 3  set  d
3 cxmt 16385 . . . . 5  class  * Met
43crn 4706 . . . 4  class  ran  * Met
54cuni 3843 . . 3  class  U. ran  * Met
6 cnx 13161 . . . . . . 7  class  ndx
7 cbs 13164 . . . . . . 7  class  Base
86, 7cfv 5271 . . . . . 6  class  ( Base `  ndx )
92cv 1631 . . . . . . . 8  class  d
109cdm 4705 . . . . . . 7  class  dom  d
1110cdm 4705 . . . . . 6  class  dom  dom  d
128, 11cop 3656 . . . . 5  class  <. ( Base `  ndx ) ,  dom  dom  d >.
13 cds 13233 . . . . . . 7  class  dist
146, 13cfv 5271 . . . . . 6  class  ( dist `  ndx )
1514, 9cop 3656 . . . . 5  class  <. ( dist `  ndx ) ,  d >.
1612, 15cpr 3654 . . . 4  class  { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. }
17 cts 13230 . . . . . 6  class TopSet
186, 17cfv 5271 . . . . 5  class  (TopSet `  ndx )
19 cmopn 16388 . . . . . 6  class  MetOpen
209, 19cfv 5271 . . . . 5  class  ( MetOpen `  d )
2118, 20cop 3656 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  d ) >.
22 csts 13162 . . . 4  class sSet
2316, 21, 22co 5874 . . 3  class  ( {
<. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. )
242, 5, 23cmpt 4093 . 2  class  ( d  e.  U. ran  * Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
251, 24wceq 1632 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 set class
This definition is referenced by:  tmsval  18043
  Copyright terms: Public domain W3C validator