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 22801
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 22798 . 2 class toUnifSp
2 vu . . 3 setvar 𝑢
3 cust 22742 . . . . 5 class UnifOn
43crn 5555 . . . 4 class ran UnifOn
54cuni 4837 . . 3 class ran UnifOn
6 cnx 16475 . . . . . . 7 class ndx
7 cbs 16478 . . . . . . 7 class Base
86, 7cfv 6354 . . . . . 6 class (Base‘ndx)
92cv 1529 . . . . . . . 8 class 𝑢
109cuni 4837 . . . . . . 7 class 𝑢
1110cdm 5554 . . . . . 6 class dom 𝑢
128, 11cop 4570 . . . . 5 class ⟨(Base‘ndx), dom 𝑢
13 cunif 16570 . . . . . . 7 class UnifSet
146, 13cfv 6354 . . . . . 6 class (UnifSet‘ndx)
1514, 9cop 4570 . . . . 5 class ⟨(UnifSet‘ndx), 𝑢
1612, 15cpr 4566 . . . 4 class {⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩}
17 cts 16566 . . . . . 6 class TopSet
186, 17cfv 6354 . . . . 5 class (TopSet‘ndx)
19 cutop 22773 . . . . . 6 class unifTop
209, 19cfv 6354 . . . . 5 class (unifTop‘𝑢)
2118, 20cop 4570 . . . 4 class ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩
22 csts 16476 . . . 4 class sSet
2316, 21, 22co 7150 . . 3 class ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩)
242, 5, 23cmpt 5143 . 2 class (𝑢 ran UnifOn ↦ ({⟨(Base‘ndx), dom 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
251, 24wceq 1530 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  22809
  Copyright terms: Public domain W3C validator