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 21985
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 21982 . 2 class toUnifSp
2 vu . . 3 setvar 𝑢
3 cust 21926 . . . . 5 class UnifOn
43crn 5080 . . . 4 class ran UnifOn
54cuni 4407 . . 3 class ran UnifOn
6 cnx 15789 . . . . . . 7 class ndx
7 cbs 15792 . . . . . . 7 class Base
86, 7cfv 5852 . . . . . 6 class (Base‘ndx)
92cv 1479 . . . . . . . 8 class 𝑢
109cuni 4407 . . . . . . 7 class 𝑢
1110cdm 5079 . . . . . 6 class dom 𝑢
128, 11cop 4159 . . . . 5 class ⟨(Base‘ndx), dom 𝑢
13 cunif 15883 . . . . . . 7 class UnifSet
146, 13cfv 5852 . . . . . 6 class (UnifSet‘ndx)
1514, 9cop 4159 . . . . 5 class ⟨(UnifSet‘ndx), 𝑢
1612, 15cpr 4155 . . . 4 class {⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩}
17 cts 15879 . . . . . 6 class TopSet
186, 17cfv 5852 . . . . 5 class (TopSet‘ndx)
19 cutop 21957 . . . . . 6 class unifTop
209, 19cfv 5852 . . . . 5 class (unifTop‘𝑢)
2118, 20cop 4159 . . . 4 class ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩
22 csts 15790 . . . 4 class sSet
2316, 21, 22co 6610 . . 3 class ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩)
242, 5, 23cmpt 4678 . 2 class (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
251, 24wceq 1480 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  21993
  Copyright terms: Public domain W3C validator