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

Definition df-tms 18352
 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 18349 . 2 toMetSp
2 vd . . 3
3 cxmt 16686 . . . . 5
43crn 4879 . . . 4
54cuni 4015 . . 3
6 cnx 13466 . . . . . . 7
7 cbs 13469 . . . . . . 7
86, 7cfv 5454 . . . . . 6
92cv 1651 . . . . . . . 8
109cdm 4878 . . . . . . 7
1110cdm 4878 . . . . . 6
128, 11cop 3817 . . . . 5
13 cds 13538 . . . . . . 7
146, 13cfv 5454 . . . . . 6
1514, 9cop 3817 . . . . 5
1612, 15cpr 3815 . . . 4
17 cts 13535 . . . . . 6 TopSet
186, 17cfv 5454 . . . . 5 TopSet
19 cmopn 16691 . . . . . 6
209, 19cfv 5454 . . . . 5
2118, 20cop 3817 . . . 4 TopSet
22 csts 13467 . . . 4 sSet
2316, 21, 22co 6081 . . 3 sSet TopSet
242, 5, 23cmpt 4266 . 2 sSet TopSet
251, 24wceq 1652 1 toMetSp sSet TopSet
 Colors of variables: wff set class This definition is referenced by:  tmsval  18511
 Copyright terms: Public domain W3C validator