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

Definition df-flim 21553
 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 21548 . 2 class fLim
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 20517 . . 3 class Top
5 cfil 21459 . . . . 5 class Fil
65crn 5039 . . . 4 class ran Fil
76cuni 4372 . . 3 class ran Fil
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1474 . . . . . . . 8 class 𝑥
109csn 4125 . . . . . . 7 class {𝑥}
112cv 1474 . . . . . . . 8 class 𝑗
12 cnei 20711 . . . . . . . 8 class nei
1311, 12cfv 5804 . . . . . . 7 class (nei‘𝑗)
1410, 13cfv 5804 . . . . . 6 class ((nei‘𝑗)‘{𝑥})
153cv 1474 . . . . . 6 class 𝑓
1614, 15wss 3540 . . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
1711cuni 4372 . . . . . . 7 class 𝑗
1817cpw 4108 . . . . . 6 class 𝒫 𝑗
1915, 18wss 3540 . . . . 5 wff 𝑓 ⊆ 𝒫 𝑗
2016, 19wa 383 . . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)
2120, 8, 17crab 2900 . . 3 class {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)}
222, 3, 4, 7, 21cmpt2 6551 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
231, 22wceq 1475 1 wff fLim = (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
 Colors of variables: wff setvar class This definition is referenced by:  flimval  21577  elflim2  21578
 Copyright terms: Public domain W3C validator