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

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

Detailed syntax breakdown of Definition df-tms
StepHypRef Expression
1 ctmt 19874 . 2
2 vd . . 3
3 cxmt 17781 . . . . 5
43crn 4836 . . . 4
54cuni 4086 . . 3
6 cnx 14163 . . . . . . 7
7 cbs 14166 . . . . . . 7
86, 7cfv 5413 . . . . . 6
92cv 1368 . . . . . . . 8
109cdm 4835 . . . . . . 7
1110cdm 4835 . . . . . 6
128, 11cop 3878 . . . . 5
13 cds 14239 . . . . . . 7
146, 13cfv 5413 . . . . . 6
1514, 9cop 3878 . . . . 5
1612, 15cpr 3874 . . . 4
17 cts 14236 . . . . . 6
186, 17cfv 5413 . . . . 5
19 cmopn 17786 . . . . . 6
209, 19cfv 5413 . . . . 5
2118, 20cop 3878 . . . 4
22 csts 14164 . . . 4
2316, 21, 22co 6086 . . 3
242, 5, 23cmpt 4345 . 2
251, 24wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  tmsval  20036
  Copyright terms: Public domain W3C validator