Definition df-flim 24258

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

Step	Hyp	Ref	Expression
1		cflim 24253	. 2 class fLim
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 23211	. . 3 class Top
5		cfil 24164	. . . . 5 class Fil
6	5	crn 5652	. . . 4 class ran Fil
7	6	cuni 4867	. . 3 class ∪ ran Fil
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1569	. . . . . . . 8 class 𝑥
10	9	csn 4584	. . . . . . 7 class {𝑥}
11	2	cv 1569	. . . . . . . 8 class 𝑗
12		cnei 23415	. . . . . . . 8 class nei
13	11, 12	cfv 6538	. . . . . . 7 class (nei‘𝑗)
14	10, 13	cfv 6538	. . . . . 6 class ((nei‘𝑗)‘{𝑥})
15	3	cv 1569	. . . . . 6 class 𝑓
16	14, 15	wss 3899	. . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
17	11	cuni 4867	. . . . . . 7 class ∪ 𝑗
18	17	cpw 4557	. . . . . 6 class 𝒫 ∪ 𝑗
19	15, 18	wss 3899	. . . . 5 wff 𝑓 ⊆ 𝒫 ∪ 𝑗
20	16, 19	wa 401	. . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)
21	20, 8, 17	crab 3413	. . 3 class {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)}
22	2, 3, 4, 7, 21	cmpo 7422	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})
23	1, 22	wceq 1570	1 wff fLim = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})

This definition is used by:  flimval  24282  elflim2  24283