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 = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccfilu	⊢ CauFilu
1		vu	⊢ 𝑢
2		cust	⊢ UnifOn
3	2	crn	⊢ ran UnifOn
4	3	cuni	⊢ ∪ ran UnifOn
5		vf	⊢ 𝑓
6		cfbas	⊢ fBas
7	1	cv	⊢ 𝑢
8	7	cuni	⊢ ∪ 𝑢
9	8	cdm	⊢ dom ∪ 𝑢
10	9 6	cfv	⊢ ( fBas ‘ dom ∪ 𝑢 )
11		vv	⊢ 𝑣
12		va	⊢ 𝑎
13	5	cv	⊢ 𝑓
14	12	cv	⊢ 𝑎
15	14 14	cxp	⊢ ( 𝑎 × 𝑎 )
16	11	cv	⊢ 𝑣
17	15 16	wss	⊢ ( 𝑎 × 𝑎 ) ⊆ 𝑣
18	17 12 13	wrex	⊢ ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣
19	18 11 7	wral	⊢ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣
20	19 5 10	crab	⊢ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 }
21	1 4 20	cmpt	⊢ ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
22	0 21	wceq	⊢ CauFilu = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )