Metamath Proof Explorer

Definition df-tms

Description: Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion df-tms 
|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctms 
 |-  toMetSp
1 vd 
 |-  d
2 cxmet 
 |-  *Met
3 2 crn 
 |-  ran *Met
4 3 cuni 
 |-  U. ran *Met
5 cbs 
 |-  Base
6 cnx 
 |-  ndx
7 6 5 cfv 
 |-  ( Base ` ndx )
8 1 cv 
 |-  d
9 8 cdm 
 |-  dom d
10 9 cdm 
 |-  dom dom d
11 7 10 cop 
 |-  <. ( Base ` ndx ) , dom dom d >.
12 cds 
 |-  dist
13 6 12 cfv 
 |-  ( dist ` ndx )
14 13 8 cop 
 |-  <. ( dist ` ndx ) , d >.
15 11 14 cpr 
 |-  { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. }
16 csts 
 |-  sSet
17 cts 
 |-  TopSet
18 6 17 cfv 
 |-  ( TopSet ` ndx )
19 cmopn 
 |-  MetOpen
20 8 19 cfv 
 |-  ( MetOpen ` d )
21 18 20 cop 
 |-  <. ( TopSet ` ndx ) , ( MetOpen ` d ) >.
22 15 21 16 co 
 |-  ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. )
23 1 4 22 cmpt 
 |-  ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
24 0 23 wceq 
 |-  toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. ( TopSet ` ndx ) , ( MetOpen ` d ) >. ) )