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

Definition df-flim 21976
Description: Define a function (indexed by a topology 𝑗) whose value is the limits of a filter 𝑓. (Contributed by Jeff Hankins, 4-Sep-2009.)
Assertion
Ref Expression
df-flim fLim = (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
Distinct variable group:   𝑓,𝑗,𝑥

Detailed syntax breakdown of Definition df-flim
StepHypRef Expression
1 cflim 21971 . 2 class fLim
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 20931 . . 3 class Top
5 cfil 21882 . . . . 5 class Fil
65crn 5325 . . . 4 class ran Fil
76cuni 4641 . . 3 class ran Fil
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1636 . . . . . . . 8 class 𝑥
109csn 4381 . . . . . . 7 class {𝑥}
112cv 1636 . . . . . . . 8 class 𝑗
12 cnei 21135 . . . . . . . 8 class nei
1311, 12cfv 6110 . . . . . . 7 class (nei‘𝑗)
1410, 13cfv 6110 . . . . . 6 class ((nei‘𝑗)‘{𝑥})
153cv 1636 . . . . . 6 class 𝑓
1614, 15wss 3780 . . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
1711cuni 4641 . . . . . . 7 class 𝑗
1817cpw 4362 . . . . . 6 class 𝒫 𝑗
1915, 18wss 3780 . . . . 5 wff 𝑓 ⊆ 𝒫 𝑗
2016, 19wa 384 . . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)
2120, 8, 17crab 3111 . . 3 class {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)}
222, 3, 4, 7, 21cmpt2 6885 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
231, 22wceq 1637 1 wff fLim = (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
Colors of variables: wff setvar class
This definition is referenced by:  flimval  22000  elflim2  22001
  Copyright terms: Public domain W3C validator