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 sSet TopSet

Detailed syntax breakdown of Definition df-tms
StepHypRef Expression
1 ctms 12402 . 2 toMetSp
2 vd . . 3
3 cxmet 12044 . . . . 5
43crn 4508 . . . 4
54cuni 3704 . . 3
6 cnx 11851 . . . . . . 7
7 cbs 11854 . . . . . . 7
86, 7cfv 5091 . . . . . 6
92cv 1313 . . . . . . . 8
109cdm 4507 . . . . . . 7
1110cdm 4507 . . . . . 6
128, 11cop 3498 . . . . 5
13 cds 11925 . . . . . . 7
146, 13cfv 5091 . . . . . 6
1514, 9cop 3498 . . . . 5
1612, 15cpr 3496 . . . 4
17 cts 11922 . . . . . 6 TopSet
186, 17cfv 5091 . . . . 5 TopSet
19 cmopn 12049 . . . . . 6
209, 19cfv 5091 . . . . 5
2118, 20cop 3498 . . . 4 TopSet
22 csts 11852 . . . 4 sSet
2316, 21, 22co 5740 . . 3 sSet TopSet
242, 5, 23cmpt 3957 . 2 sSet TopSet
251, 24wceq 1314 1 toMetSp sSet TopSet
 Colors of variables: wff set class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator