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

Definition df-tms 21415
 Description: Define the function mapping a metric to a metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
df-tms toMetSp sSet TopSet

Detailed syntax breakdown of Definition df-tms
StepHypRef Expression
1 ctmt 21412 . 2 toMetSp
2 vd . . 3
3 cxmt 19032 . . . . 5
43crn 4840 . . . 4
54cuni 4190 . . 3
6 cnx 15196 . . . . . . 7
7 cbs 15199 . . . . . . 7
86, 7cfv 5589 . . . . . 6
92cv 1451 . . . . . . . 8
109cdm 4839 . . . . . . 7
1110cdm 4839 . . . . . 6
128, 11cop 3965 . . . . 5
13 cds 15277 . . . . . . 7
146, 13cfv 5589 . . . . . 6
1514, 9cop 3965 . . . . 5
1612, 15cpr 3961 . . . 4
17 cts 15274 . . . . . 6 TopSet
186, 17cfv 5589 . . . . 5 TopSet
19 cmopn 19037 . . . . . 6
209, 19cfv 5589 . . . . 5
2118, 20cop 3965 . . . 4 TopSet
22 csts 15197 . . . 4 sSet
2316, 21, 22co 6308 . . 3 sSet TopSet
242, 5, 23cmpt 4454 . 2 sSet TopSet
251, 24wceq 1452 1 toMetSp sSet TopSet
 Colors of variables: wff setvar class This definition is referenced by:  tmsval  21574
 Copyright terms: Public domain W3C validator