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

Definition df-tus 22432
Description: Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.)
Assertion
Ref Expression
df-tus toUnifSp = (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))

Detailed syntax breakdown of Definition df-tus
StepHypRef Expression
1 ctus 22429 . 2 class toUnifSp
2 vu . . 3 setvar 𝑢
3 cust 22373 . . . . 5 class UnifOn
43crn 5343 . . . 4 class ran UnifOn
54cuni 4658 . . 3 class ran UnifOn
6 cnx 16219 . . . . . . 7 class ndx
7 cbs 16222 . . . . . . 7 class Base
86, 7cfv 6123 . . . . . 6 class (Base‘ndx)
92cv 1655 . . . . . . . 8 class 𝑢
109cuni 4658 . . . . . . 7 class 𝑢
1110cdm 5342 . . . . . 6 class dom 𝑢
128, 11cop 4403 . . . . 5 class ⟨(Base‘ndx), dom 𝑢
13 cunif 16315 . . . . . . 7 class UnifSet
146, 13cfv 6123 . . . . . 6 class (UnifSet‘ndx)
1514, 9cop 4403 . . . . 5 class ⟨(UnifSet‘ndx), 𝑢
1612, 15cpr 4399 . . . 4 class {⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩}
17 cts 16311 . . . . . 6 class TopSet
186, 17cfv 6123 . . . . 5 class (TopSet‘ndx)
19 cutop 22404 . . . . . 6 class unifTop
209, 19cfv 6123 . . . . 5 class (unifTop‘𝑢)
2118, 20cop 4403 . . . 4 class ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩
22 csts 16220 . . . 4 class sSet
2316, 21, 22co 6905 . . 3 class ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩)
242, 5, 23cmpt 4952 . 2 class (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
251, 24wceq 1656 1 wff toUnifSp = (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  tusval  22440
  Copyright terms: Public domain W3C validator