MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fil Structured version   Visualization version   GIF version

Definition df-fil 22384
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
StepHypRef Expression
1 cfil 22383 . 2 class Fil
2 vz . . 3 setvar 𝑧
3 cvv 3495 . . 3 class V
4 vf . . . . . . . . 9 setvar 𝑓
54cv 1527 . . . . . . . 8 class 𝑓
6 vx . . . . . . . . . 10 setvar 𝑥
76cv 1527 . . . . . . . . 9 class 𝑥
87cpw 4537 . . . . . . . 8 class 𝒫 𝑥
95, 8cin 3934 . . . . . . 7 class (𝑓 ∩ 𝒫 𝑥)
10 c0 4290 . . . . . . 7 class
119, 10wne 3016 . . . . . 6 wff (𝑓 ∩ 𝒫 𝑥) ≠ ∅
126, 4wel 2106 . . . . . 6 wff 𝑥𝑓
1311, 12wi 4 . . . . 5 wff ((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝑓)
142cv 1527 . . . . . 6 class 𝑧
1514cpw 4537 . . . . 5 class 𝒫 𝑧
1613, 6, 15wral 3138 . . . 4 wff 𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝑓)
17 cfbas 20463 . . . . 5 class fBas
1814, 17cfv 6349 . . . 4 class (fBas‘𝑧)
1916, 4, 18crab 3142 . . 3 class {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝑓)}
202, 3, 19cmpt 5138 . 2 class (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝑓)})
211, 20wceq 1528 1 wff Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝑓)})
Colors of variables: wff setvar class
This definition is referenced by:  isfil  22385  filunirn  22420
  Copyright terms: Public domain W3C validator