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

Definition df-tms 24347
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 = (𝑑 ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))

Detailed syntax breakdown of Definition df-tms
StepHypRef Expression
1 ctms 24344 . 2 class toMetSp
2 vd . . 3 setvar 𝑑
3 cxmet 21366 . . . . 5 class ∞Met
43crn 5689 . . . 4 class ran ∞Met
54cuni 4911 . . 3 class ran ∞Met
6 cnx 17226 . . . . . . 7 class ndx
7 cbs 17244 . . . . . . 7 class Base
86, 7cfv 6562 . . . . . 6 class (Base‘ndx)
92cv 1535 . . . . . . . 8 class 𝑑
109cdm 5688 . . . . . . 7 class dom 𝑑
1110cdm 5688 . . . . . 6 class dom dom 𝑑
128, 11cop 4636 . . . . 5 class ⟨(Base‘ndx), dom dom 𝑑
13 cds 17306 . . . . . . 7 class dist
146, 13cfv 6562 . . . . . 6 class (dist‘ndx)
1514, 9cop 4636 . . . . 5 class ⟨(dist‘ndx), 𝑑
1612, 15cpr 4632 . . . 4 class {⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩}
17 cts 17303 . . . . . 6 class TopSet
186, 17cfv 6562 . . . . 5 class (TopSet‘ndx)
19 cmopn 21371 . . . . . 6 class MetOpen
209, 19cfv 6562 . . . . 5 class (MetOpen‘𝑑)
2118, 20cop 4636 . . . 4 class ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩
22 csts 17196 . . . 4 class sSet
2316, 21, 22co 7430 . . 3 class ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩)
242, 5, 23cmpt 5230 . 2 class (𝑑 ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
251, 24wceq 1536 1 wff toMetSp = (𝑑 ran ∞Met ↦ ({⟨(Base‘ndx), dom dom 𝑑⟩, ⟨(dist‘ndx), 𝑑⟩} sSet ⟨(TopSet‘ndx), (MetOpen‘𝑑)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  tmsval  24508
  Copyright terms: Public domain W3C validator