Definition df-tus

Description: Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017)

	Ref	Expression
Assertion	df-tus	$$⊢\mathrm{toUnifSp}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(u\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctus	$$class\mathrm{toUnifSp}$$
1		vu	$$setvaru$$
2		cust	$$class\mathrm{UnifOn}$$
3	2	crn	$$class\mathrm{ran}\mathrm{UnifOn}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{UnifOn}$$
5		cbs	$$class\mathrm{Base}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
8	1	cv	$$setvaru$$
9	8	cuni	$$class\bigcup u$$
10	9	cdm	$$class\mathrm{dom}\bigcup u$$
11	7 10	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩$$
12		cunif	$$class\mathrm{UnifSet}$$
13	6 12	cfv	$$class\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
14	13 8	cop	$$class⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩$$
15	11 14	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩\right\}$$
16		csts	$$class\mathrm{sSet}$$
17		cts	$$class\mathrm{TopSet}$$
18	6 17	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
19		cutop	$$class\mathrm{unifTop}$$
20	8 19	cfv	$$class\mathrm{unifTop}\left(u\right)$$
21	18 20	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(u\right)⟩$$
22	15 21 16	co	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(u\right)⟩\right)$$
23	1 4 22	cmpt	$$class\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(u\right)⟩\right)$$
24	0 23	wceq	$$wff\mathrm{toUnifSp}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup u⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),u⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(u\right)⟩\right)$$