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

Definition df-tus 21872
 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 21869 . 2 class toUnifSp
2 vu . . 3 setvar 𝑢
3 cust 21813 . . . . 5 class UnifOn
43crn 5039 . . . 4 class ran UnifOn
54cuni 4372 . . 3 class ran UnifOn
6 cnx 15692 . . . . . . 7 class ndx
7 cbs 15695 . . . . . . 7 class Base
86, 7cfv 5804 . . . . . 6 class (Base‘ndx)
92cv 1474 . . . . . . . 8 class 𝑢
109cuni 4372 . . . . . . 7 class 𝑢
1110cdm 5038 . . . . . 6 class dom 𝑢
128, 11cop 4131 . . . . 5 class ⟨(Base‘ndx), dom 𝑢
13 cunif 15778 . . . . . . 7 class UnifSet
146, 13cfv 5804 . . . . . 6 class (UnifSet‘ndx)
1514, 9cop 4131 . . . . 5 class ⟨(UnifSet‘ndx), 𝑢
1612, 15cpr 4127 . . . 4 class {⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩}
17 cts 15774 . . . . . 6 class TopSet
186, 17cfv 5804 . . . . 5 class (TopSet‘ndx)
19 cutop 21844 . . . . . 6 class unifTop
209, 19cfv 5804 . . . . 5 class (unifTop‘𝑢)
2118, 20cop 4131 . . . 4 class ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩
22 csts 15693 . . . 4 class sSet
2316, 21, 22co 6549 . . 3 class ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩)
242, 5, 23cmpt 4643 . 2 class (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
251, 24wceq 1475 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  21880
 Copyright terms: Public domain W3C validator