Definition df-fil 23749

Description: The set of filters on a set. Definition 1 (axioms FI, FIIa, FIIb, FIII) of [BourbakiTop1] p. I.36. Filters are used to define the concept of limit in the general case. They are a generalization of the idea of neighborhoods. Suppose you are in ℝ. With neighborhoods you can express the idea of a variable that tends to a specific number but you can't express the idea of a variable that tends to infinity. Filters relax the "axioms" of neighborhoods and then succeed in expressing the idea of something that tends to infinity. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)

Assertion

Ref	Expression
df-fil	⊢ Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)})

Distinct variable group:   𝑥,𝑓,𝑧

Detailed syntax breakdown of Definition df-fil

Step	Hyp	Ref	Expression
1		cfil 23748	. 2 class Fil
2		vz	. . 3 setvar 𝑧
3		cvv 3438	. . 3 class V
4		vf	. . . . . . . . 9 setvar 𝑓
5	4	cv 1539	. . . . . . . 8 class 𝑓
6		vx	. . . . . . . . . 10 setvar 𝑥
7	6	cv 1539	. . . . . . . . 9 class 𝑥
8	7	cpw 4553	. . . . . . . 8 class 𝒫 𝑥
9	5, 8	cin 3904	. . . . . . 7 class (𝑓 ∩ 𝒫 𝑥)
10		c0 4286	. . . . . . 7 class ∅
11	9, 10	wne 2925	. . . . . 6 wff (𝑓 ∩ 𝒫 𝑥) ≠ ∅
12	6, 4	wel 2110	. . . . . 6 wff 𝑥 ∈ 𝑓
13	11, 12	wi 4	. . . . 5 wff ((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)
14	2	cv 1539	. . . . . 6 class 𝑧
15	14	cpw 4553	. . . . 5 class 𝒫 𝑧
16	13, 6, 15	wral 3044	. . . 4 wff ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)
17		cfbas 21267	. . . . 5 class fBas
18	14, 17	cfv 6486	. . . 4 class (fBas‘𝑧)
19	16, 4, 18	crab 3396	. . 3 class {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)}
20	2, 3, 19	cmpt 5176	. 2 class (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)})
21	1, 20	wceq 1540	1 wff Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)})

This definition is referenced by:  isfil  23750  filunirn  23785