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

Definition df-flim 22644
 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 22639 . 2 class fLim
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 21598 . . 3 class Top
5 cfil 22550 . . . . 5 class Fil
65crn 5528 . . . 4 class ran Fil
76cuni 4801 . . 3 class ran Fil
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1537 . . . . . . . 8 class 𝑥
109csn 4525 . . . . . . 7 class {𝑥}
112cv 1537 . . . . . . . 8 class 𝑗
12 cnei 21802 . . . . . . . 8 class nei
1311, 12cfv 6339 . . . . . . 7 class (nei‘𝑗)
1410, 13cfv 6339 . . . . . 6 class ((nei‘𝑗)‘{𝑥})
153cv 1537 . . . . . 6 class 𝑓
1614, 15wss 3860 . . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
1711cuni 4801 . . . . . . 7 class 𝑗
1817cpw 4497 . . . . . 6 class 𝒫 𝑗
1915, 18wss 3860 . . . . 5 wff 𝑓 ⊆ 𝒫 𝑗
2016, 19wa 399 . . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)
2120, 8, 17crab 3074 . . 3 class {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)}
222, 3, 4, 7, 21cmpo 7157 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
231, 22wceq 1538 1 wff fLim = (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
 Colors of variables: wff setvar class This definition is referenced by:  flimval  22668  elflim2  22669
 Copyright terms: Public domain W3C validator