| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-fil | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-fil | ⊢ Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cfil 23853 | . 2 class Fil | |
| 2 | vz | . . 3 setvar 𝑧 | |
| 3 | cvv 3480 | . . 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 4600 | . . . . . . . 8 class 𝒫 𝑥 |
| 9 | 5, 8 | cin 3950 | . . . . . . 7 class (𝑓 ∩ 𝒫 𝑥) |
| 10 | c0 4333 | . . . . . . 7 class ∅ | |
| 11 | 9, 10 | wne 2940 | . . . . . 6 wff (𝑓 ∩ 𝒫 𝑥) ≠ ∅ |
| 12 | 6, 4 | wel 2109 | . . . . . 6 wff 𝑥 ∈ 𝑓 |
| 13 | 11, 12 | wi 4 | . . . . 5 wff ((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓) |
| 14 | 2 | cv 1539 | . . . . . 6 class 𝑧 |
| 15 | 14 | cpw 4600 | . . . . 5 class 𝒫 𝑧 |
| 16 | 13, 6, 15 | wral 3061 | . . . 4 wff ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓) |
| 17 | cfbas 21352 | . . . . 5 class fBas | |
| 18 | 14, 17 | cfv 6561 | . . . 4 class (fBas‘𝑧) |
| 19 | 16, 4, 18 | crab 3436 | . . 3 class {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)} |
| 20 | 2, 3, 19 | cmpt 5225 | . 2 class (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)}) |
| 21 | 1, 20 | wceq 1540 | 1 wff Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: isfil 23855 filunirn 23890 |
| Copyright terms: Public domain | W3C validator |