Definition df-tus 22062

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 = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. (TopSet ` ndx ) , (unifTop ` u ) >. ) )

Detailed syntax breakdown of Definition df-tus

Step	Hyp	Ref	Expression
1		ctus 22059	. 2 class toUnifSp
2		vu	. . 3 setvar u
3		cust 22003	. . . . 5 class UnifOn
4	3	crn 5115	. . . 4 class ran UnifOn
5	4	cuni 4436	. . 3 class U. ran UnifOn
6		cnx 15854	. . . . . . 7 class ndx
7		cbs 15857	. . . . . . 7 class Base
8	6, 7	cfv 5888	. . . . . 6 class ( Base ` ndx )
9	2	cv 1482	. . . . . . . 8 class u
10	9	cuni 4436	. . . . . . 7 class U. u
11	10	cdm 5114	. . . . . 6 class dom U. u
12	8, 11	cop 4183	. . . . 5 class <. ( Base ` ndx ) , dom U. u >.
13		cunif 15951	. . . . . . 7 class UnifSet
14	6, 13	cfv 5888	. . . . . 6 class ( UnifSet ` ndx )
15	14, 9	cop 4183	. . . . 5 class <. ( UnifSet ` ndx ) , u >.
16	12, 15	cpr 4179	. . . 4 class { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. }
17		cts 15947	. . . . . 6 class TopSet
18	6, 17	cfv 5888	. . . . 5 class (TopSet ` ndx )
19		cutop 22034	. . . . . 6 class unifTop
20	9, 19	cfv 5888	. . . . 5 class (unifTop ` u )
21	18, 20	cop 4183	. . . 4 class <. (TopSet ` ndx ) , (unifTop ` u ) >.
22		csts 15855	. . . 4 class sSet
23	16, 21, 22	co 6650	. . 3 class ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. (TopSet ` ndx ) , (unifTop ` u ) >. )
24	2, 5, 23	cmpt 4729	. 2 class ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. (TopSet ` ndx ) , (unifTop ` u ) >. ) )
25	1, 24	wceq 1483	1 wff toUnifSp = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. (TopSet ` ndx ) , (unifTop ` u ) >. ) )

This definition is referenced by:  tusval  22070