Definition df-cfilu 22091

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.)

Assertion

Ref	Expression
df-cfilu	|- CauFilu = ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )

Distinct variable group:   u, f, v, a

Detailed syntax breakdown of Definition df-cfilu

Step	Hyp	Ref	Expression
1		ccfilu 22090	. 2 class CauFilu
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		va	. . . . . . . . 9 setvar a
7	6	cv 1482	. . . . . . . 8 class a
8	7, 7	cxp 5112	. . . . . . 7 class ( a X. a )
9		vv	. . . . . . . 8 setvar v
10	9	cv 1482	. . . . . . 7 class v
11	8, 10	wss 3574	. . . . . 6 wff ( a X. a ) C_ v
12		vf	. . . . . . 7 setvar f
13	12	cv 1482	. . . . . 6 class f
14	11, 6, 13	wrex 2913	. . . . 5 wff E. a e. f ( a X. a ) C_ v
15	2	cv 1482	. . . . 5 class u
16	14, 9, 15	wral 2912	. . . 4 wff A. v e. u E. a e. f ( a X. a ) C_ v
17	15	cuni 4436	. . . . . 6 class U. u
18	17	cdm 5114	. . . . 5 class dom U. u
19		cfbas 19734	. . . . 5 class fBas
20	18, 19	cfv 5888	. . . 4 class ( fBas ` dom U. u )
21	16, 12, 20	crab 2916	. . 3 class { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v }
22	2, 5, 21	cmpt 4729	. 2 class ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )
23	1, 22	wceq 1483	1 wff CauFilu = ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )

This definition is referenced by:  iscfilu  22092