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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfilu	|- CauFilU
1		vu	|- u
2		cust	|- UnifOn
3	2	crn	|- ran UnifOn
4	3	cuni	|- U. ran UnifOn
5		vf	|- f
6		cfbas	|- fBas
7	1	cv	|- u
8	7	cuni	|- U. u
9	8	cdm	|- dom U. u
10	9 6	cfv	|- ( fBas ` dom U. u )
11		vv	|- v
12		va	|- a
13	5	cv	|- f
14	12	cv	|- a
15	14 14	cxp	|- ( a X. a )
16	11	cv	|- v
17	15 16	wss	|- ( a X. a ) C_ v
18	17 12 13	wrex	|- E. a e. f ( a X. a ) C_ v
19	18 11 7	wral	|- A. v e. u E. a e. f ( a X. a ) C_ v
20	19 5 10	crab	|- { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v }
21	1 4 20	cmpt	|- ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )
22	0 21	wceq	|- 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 } )