Definition df-cfilu 24513

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 𝑣, there is an element 𝑎 of the filter "small enough in 𝑣 " i.e. such that every pair {𝑥, 𝑦} of points in 𝑎 is related by 𝑣". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)

Assertion

Ref	Expression
df-cfilu	⊢ CauFilu = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣})

Distinct variable group:   𝑢,𝑓,𝑣,𝑎

Detailed syntax breakdown of Definition df-cfilu

Step	Hyp	Ref	Expression
1		ccfilu 24512	. 2 class CauFilu
2		vu	. . 3 setvar 𝑢
3		cust 24427	. . . . 5 class UnifOn
4	3	crn 5656	. . . 4 class ran UnifOn
5	4	cuni 4867	. . 3 class ∪ ran UnifOn
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1569	. . . . . . . 8 class 𝑎
8	7, 7	cxp 5653	. . . . . . 7 class (𝑎 × 𝑎)
9		vv	. . . . . . . 8 setvar 𝑣
10	9	cv 1569	. . . . . . 7 class 𝑣
11	8, 10	wss 3899	. . . . . 6 wff (𝑎 × 𝑎) ⊆ 𝑣
12		vf	. . . . . . 7 setvar 𝑓
13	12	cv 1569	. . . . . 6 class 𝑓
14	11, 6, 13	wrex 3086	. . . . 5 wff ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣
15	2	cv 1569	. . . . 5 class 𝑢
16	14, 9, 15	wral 3076	. . . 4 wff ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣
17	15	cuni 4867	. . . . . 6 class ∪ 𝑢
18	17	cdm 5655	. . . . 5 class dom ∪ 𝑢
19		cfbas 21574	. . . . 5 class fBas
20	18, 19	cfv 6533	. . . 4 class (fBas‘dom ∪ 𝑢)
21	16, 12, 20	crab 3412	. . 3 class {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣}
22	2, 5, 21	cmpt 5186	. 2 class (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
23	1, 22	wceq 1570	1 wff CauFilu = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (fBas‘dom ∪ 𝑢) ∣ ∀𝑣 ∈ 𝑢 ∃𝑎 ∈ 𝑓 (𝑎 × 𝑎) ⊆ 𝑣})

This definition is used by:  iscfilu  24514