Definition df-utop

Description: Definition of a topology induced by a uniform structure. Definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

	Ref	Expression
Assertion	df-utop	$$⊢\mathrm{unifTop}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{a\in 𝒫\mathrm{dom}\bigcup u|\forall x\in a\exists v\in uv\left[\left\{x\right\}\right]\subseteq a\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cutop	$$class\mathrm{unifTop}$$
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		va	$$setvara$$
6	1	cv	$$setvaru$$
7	6	cuni	$$class\bigcup u$$
8	7	cdm	$$class\mathrm{dom}\bigcup u$$
9	8	cpw	$$class𝒫\mathrm{dom}\bigcup u$$
10		vx	$$setvarx$$
11	5	cv	$$setvara$$
12		vv	$$setvarv$$
13	12	cv	$$setvarv$$
14	10	cv	$$setvarx$$
15	14	csn	$$class\left\{x\right\}$$
16	13 15	cima	$$classv\left[\left\{x\right\}\right]$$
17	16 11	wss	$$wffv\left[\left\{x\right\}\right]\subseteq a$$
18	17 12 6	wrex	$$wff\exists v\in uv\left[\left\{x\right\}\right]\subseteq a$$
19	18 10 11	wral	$$wff\forall x\in a\exists v\in uv\left[\left\{x\right\}\right]\subseteq a$$
20	19 5 9	crab	$$class\left\{a\in 𝒫\mathrm{dom}\bigcup u|\forall x\in a\exists v\in uv\left[\left\{x\right\}\right]\subseteq a\right\}$$
21	1 4 20	cmpt	$$class\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{a\in 𝒫\mathrm{dom}\bigcup u|\forall x\in a\exists v\in uv\left[\left\{x\right\}\right]\subseteq a\right\}\right)$$
22	0 21	wceq	$$wff\mathrm{unifTop}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{a\in 𝒫\mathrm{dom}\bigcup u|\forall x\in a\exists v\in uv\left[\left\{x\right\}\right]\subseteq a\right\}\right)$$