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

Step	Hyp	Ref	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
6	5	crn 5039	. . . 4 class ran Fil
7	6	cuni 4372	. . 3 class ∪ ran Fil
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1474	. . . . . . . 8 class 𝑥
10	9	csn 4125	. . . . . . 7 class {𝑥}
11	2	cv 1474	. . . . . . . 8 class 𝑗
12		cnei 20711	. . . . . . . 8 class nei
13	11, 12	cfv 5804	. . . . . . 7 class (nei‘𝑗)
14	10, 13	cfv 5804	. . . . . 6 class ((nei‘𝑗)‘{𝑥})
15	3	cv 1474	. . . . . 6 class 𝑓
16	14, 15	wss 3540	. . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
17	11	cuni 4372	. . . . . . 7 class ∪ 𝑗
18	17	cpw 4108	. . . . . 6 class 𝒫 ∪ 𝑗
19	15, 18	wss 3540	. . . . 5 wff 𝑓 ⊆ 𝒫 ∪ 𝑗
20	16, 19	wa 383	. . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)
21	20, 8, 17	crab 2900	. . 3 class {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)}
22	2, 3, 4, 7, 21	cmpt2 6551	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})
23	1, 22	wceq 1475	1 wff fLim = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})

This definition is referenced by:  flimval  21577  elflim2  21578