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

Definition df-tms 12405
Description: Define the function mapping a metric to the metric space which it defines. (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 ctms 12402 . 2  class toMetSp
2 vd . . 3  setvar  d
3 cxmet 12044 . . . . 5  class  *Met
43crn 4508 . . . 4  class  ran  *Met
54cuni 3704 . . 3  class  U. ran  *Met
6 cnx 11851 . . . . . . 7  class  ndx
7 cbs 11854 . . . . . . 7  class  Base
86, 7cfv 5091 . . . . . 6  class  ( Base `  ndx )
92cv 1313 . . . . . . . 8  class  d
109cdm 4507 . . . . . . 7  class  dom  d
1110cdm 4507 . . . . . 6  class  dom  dom  d
128, 11cop 3498 . . . . 5  class  <. ( Base `  ndx ) ,  dom  dom  d >.
13 cds 11925 . . . . . . 7  class  dist
146, 13cfv 5091 . . . . . 6  class  ( dist `  ndx )
1514, 9cop 3498 . . . . 5  class  <. ( dist `  ndx ) ,  d >.
1612, 15cpr 3496 . . . 4  class  { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. }
17 cts 11922 . . . . . 6  class TopSet
186, 17cfv 5091 . . . . 5  class  (TopSet `  ndx )
19 cmopn 12049 . . . . . 6  class  MetOpen
209, 19cfv 5091 . . . . 5  class  ( MetOpen `  d )
2118, 20cop 3498 . . . 4  class  <. (TopSet ` 
ndx ) ,  (
MetOpen `  d ) >.
22 csts 11852 . . . 4  class sSet
2316, 21, 22co 5740 . . 3  class  ( {
<. ( Base `  ndx ) ,  dom  dom  d >. ,  <. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. )
242, 5, 23cmpt 3957 . 2  class  ( d  e.  U. ran  *Met  |->  ( { <. (
Base `  ndx ) ,  dom  dom  d >. , 
<. ( dist `  ndx ) ,  d >. } sSet  <. (TopSet `  ndx ) ,  ( MetOpen `  d ) >. ) )
251, 24wceq 1314 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: (None)
  Copyright terms: Public domain W3C validator