Definition df-tus 22869

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

Step	Hyp	Ref	Expression
1		ctus 22866	. 2 class toUnifSp
2		vu	. . 3 setvar 𝑢
3		cust 22810	. . . . 5 class UnifOn
4	3	crn 5558	. . . 4 class ran UnifOn
5	4	cuni 4840	. . 3 class ∪ ran UnifOn
6		cnx 16482	. . . . . . 7 class ndx
7		cbs 16485	. . . . . . 7 class Base
8	6, 7	cfv 6357	. . . . . 6 class (Base‘ndx)
9	2	cv 1536	. . . . . . . 8 class 𝑢
10	9	cuni 4840	. . . . . . 7 class ∪ 𝑢
11	10	cdm 5557	. . . . . 6 class dom ∪ 𝑢
12	8, 11	cop 4575	. . . . 5 class ⟨(Base‘ndx), dom ∪ 𝑢⟩
13		cunif 16577	. . . . . . 7 class UnifSet
14	6, 13	cfv 6357	. . . . . 6 class (UnifSet‘ndx)
15	14, 9	cop 4575	. . . . 5 class ⟨(UnifSet‘ndx), 𝑢⟩
16	12, 15	cpr 4571	. . . 4 class {⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩}
17		cts 16573	. . . . . 6 class TopSet
18	6, 17	cfv 6357	. . . . 5 class (TopSet‘ndx)
19		cutop 22841	. . . . . 6 class unifTop
20	9, 19	cfv 6357	. . . . 5 class (unifTop‘𝑢)
21	18, 20	cop 4575	. . . 4 class ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩
22		csts 16483	. . . 4 class sSet
23	16, 21, 22	co 7158	. . 3 class ({⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩)
24	2, 5, 23	cmpt 5148	. 2 class (𝑢 ∈ ∪ ran UnifOn ↦ ({⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))
25	1, 24	wceq 1537	1 wff toUnifSp = (𝑢 ∈ ∪ ran UnifOn ↦ ({⟨(Base‘ndx), dom ∪ 𝑢⟩, ⟨(UnifSet‘ndx), 𝑢⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑢)⟩))

This definition is referenced by:  tusval  22877