Metamath Proof Explorer

Definition df-fil

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

Ref Expression
Assertion df-fil ⊢ Fil = z ∈ V ⟼ f ∈ fBas ⁡ z | ∀ x ∈ 𝒫 z f ∩ 𝒫 x ≠ ∅ → x ∈ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfil class Fil
1 vz setvar z
2 cvv class V
3 vf setvar f
4 cfbas class fBas
5 1 cv setvar z
6 5 4 cfv class fBas ⁡ z
7 vx setvar x
8 5 cpw class 𝒫 z
9 3 cv setvar f
10 7 cv setvar x
11 10 cpw class 𝒫 x
12 9 11 cin class f ∩ 𝒫 x
13 c0 class ∅
14 12 13 wne wff f ∩ 𝒫 x ≠ ∅
15 10 9 wcel wff x ∈ f
16 14 15 wi wff f ∩ 𝒫 x ≠ ∅ → x ∈ f
17 16 7 8 wral wff ∀ x ∈ 𝒫 z f ∩ 𝒫 x ≠ ∅ → x ∈ f
18 17 3 6 crab class f ∈ fBas ⁡ z | ∀ x ∈ 𝒫 z f ∩ 𝒫 x ≠ ∅ → x ∈ f
19 1 2 18 cmpt class z ∈ V ⟼ f ∈ fBas ⁡ z | ∀ x ∈ 𝒫 z f ∩ 𝒫 x ≠ ∅ → x ∈ f
20 0 19 wceq wff Fil = z ∈ V ⟼ f ∈ fBas ⁡ z | ∀ x ∈ 𝒫 z f ∩ 𝒫 x ≠ ∅ → x ∈ f