Definition df-flim 23372

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 23367	. 2 class fLim
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 22324	. . 3 class Top
5		cfil 23278	. . . . 5 class Fil
6	5	crn 5670	. . . 4 class ran Fil
7	6	cuni 4901	. . 3 class ∪ ran Fil
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1540	. . . . . . . 8 class 𝑥
10	9	csn 4622	. . . . . . 7 class {𝑥}
11	2	cv 1540	. . . . . . . 8 class 𝑗
12		cnei 22530	. . . . . . . 8 class nei
13	11, 12	cfv 6532	. . . . . . 7 class (nei‘𝑗)
14	10, 13	cfv 6532	. . . . . 6 class ((nei‘𝑗)‘{𝑥})
15	3	cv 1540	. . . . . 6 class 𝑓
16	14, 15	wss 3944	. . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
17	11	cuni 4901	. . . . . . 7 class ∪ 𝑗
18	17	cpw 4596	. . . . . 6 class 𝒫 ∪ 𝑗
19	15, 18	wss 3944	. . . . 5 wff 𝑓 ⊆ 𝒫 ∪ 𝑗
20	16, 19	wa 396	. . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)
21	20, 8, 17	crab 3431	. . 3 class {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)}
22	2, 3, 4, 7, 21	cmpo 7395	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})
23	1, 22	wceq 1541	1 wff fLim = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})

This definition is referenced by:  flimval  23396  elflim2  23397