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

Definition df-tms 17882
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 17879 . 2  class toMetSp
2 vd . . 3  set  d
3 cxmt 16364 . . . . 5  class  * Met
43crn 4690 . . . 4  class  ran  * Met
54cuni 3829 . . 3  class  U. ran  * Met
6 cnx 13140 . . . . . . 7  class  ndx
7 cbs 13143 . . . . . . 7  class  Base
86, 7cfv 5222 . . . . . 6  class  ( Base `  ndx )
92cv 1623 . . . . . . . 8  class  d
109cdm 4689 . . . . . . 7  class  dom  d
1110cdm 4689 . . . . . 6  class  dom  dom  d
128, 11cop 3645 . . . . 5  class  <. ( Base `  ndx ) ,  dom  dom  d >.
13 cds 13212 . . . . . . 7  class  dist
146, 13cfv 5222 . . . . . 6  class  ( dist `  ndx )
1514, 9cop 3645 . . . . 5  class  <. ( dist `  ndx ) ,  d >.
1612, 15cpr 3643 . . . 4  class  { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. }
17 cts 13209 . . . . . 6  class TopSet
186, 17cfv 5222 . . . . 5  class  (TopSet `  ndx )
19 cmopn 16367 . . . . . 6  class  MetOpen
209, 19cfv 5222 . . . . 5  class  ( MetOpen `  d )
2118, 20cop 3645 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  d ) >.
22 csts 13141 . . . 4  class sSet
2316, 21, 22co 5820 . . 3  class  ( {
<. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. )
242, 5, 23cmpt 4079 . 2  class  ( d  e.  U. ran  * Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
251, 24wceq 1624 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  18022
  Copyright terms: Public domain W3C validator