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 22477
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 22472 . 2 class fLim
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 21431 . . 3 class Top
5 cfil 22383 . . . . 5 class Fil
65crn 5550 . . . 4 class ran Fil
76cuni 4832 . . 3 class ran Fil
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1527 . . . . . . . 8 class 𝑥
109csn 4559 . . . . . . 7 class {𝑥}
112cv 1527 . . . . . . . 8 class 𝑗
12 cnei 21635 . . . . . . . 8 class nei
1311, 12cfv 6349 . . . . . . 7 class (nei‘𝑗)
1410, 13cfv 6349 . . . . . 6 class ((nei‘𝑗)‘{𝑥})
153cv 1527 . . . . . 6 class 𝑓
1614, 15wss 3935 . . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
1711cuni 4832 . . . . . . 7 class 𝑗
1817cpw 4537 . . . . . 6 class 𝒫 𝑗
1915, 18wss 3935 . . . . 5 wff 𝑓 ⊆ 𝒫 𝑗
2016, 19wa 396 . . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)
2120, 8, 17crab 3142 . . 3 class {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)}
222, 3, 4, 7, 21cmpo 7147 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
231, 22wceq 1528 1 wff fLim = (𝑗 ∈ Top, 𝑓 ran Fil ↦ {𝑥 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓𝑓 ⊆ 𝒫 𝑗)})
Colors of variables: wff setvar class
This definition is referenced by:  flimval  22501  elflim2  22502
  Copyright terms: Public domain W3C validator