Definition df-cfilu

Description: Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage v , there is an element a of the filter "small enough in v " i.e. such that every pair { x , y } of points in a is related by v ". Definition 2 of BourbakiTop1 p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017)

	Ref	Expression
Assertion	df-cfilu	$$⊢\mathrm{CauFilU}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{f\in \mathrm{fBas}\left(\mathrm{dom}\bigcup u\right)|\forall v\in u\exists a\in fa\times a\subseteq v\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfilu	$$class\mathrm{CauFilU}$$
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		vf	$$setvarf$$
6		cfbas	$$class\mathrm{fBas}$$
7	1	cv	$$setvaru$$
8	7	cuni	$$class\bigcup u$$
9	8	cdm	$$class\mathrm{dom}\bigcup u$$
10	9 6	cfv	$$class\mathrm{fBas}\left(\mathrm{dom}\bigcup u\right)$$
11		vv	$$setvarv$$
12		va	$$setvara$$
13	5	cv	$$setvarf$$
14	12	cv	$$setvara$$
15	14 14	cxp	$$class\left(a\times a\right)$$
16	11	cv	$$setvarv$$
17	15 16	wss	$$wffa\times a\subseteq v$$
18	17 12 13	wrex	$$wff\exists a\in fa\times a\subseteq v$$
19	18 11 7	wral	$$wff\forall v\in u\exists a\in fa\times a\subseteq v$$
20	19 5 10	crab	$$class\left\{f\in \mathrm{fBas}\left(\mathrm{dom}\bigcup u\right)|\forall v\in u\exists a\in fa\times a\subseteq v\right\}$$
21	1 4 20	cmpt	$$class\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{f\in \mathrm{fBas}\left(\mathrm{dom}\bigcup u\right)|\forall v\in u\exists a\in fa\times a\subseteq v\right\}\right)$$
22	0 21	wceq	$$wff\mathrm{CauFilU}=\left(u\in \bigcup \mathrm{ran}\mathrm{UnifOn}⟼\left\{f\in \mathrm{fBas}\left(\mathrm{dom}\bigcup u\right)|\forall v\in u\exists a\in fa\times a\subseteq v\right\}\right)$$