Definition df-flim 22547

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 22542	. 2 class fLim
2		vj	. . 3 setvar 𝑗
3		vf	. . 3 setvar 𝑓
4		ctop 21501	. . 3 class Top
5		cfil 22453	. . . . 5 class Fil
6	5	crn 5556	. . . 4 class ran Fil
7	6	cuni 4838	. . 3 class ∪ ran Fil
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1536	. . . . . . . 8 class 𝑥
10	9	csn 4567	. . . . . . 7 class {𝑥}
11	2	cv 1536	. . . . . . . 8 class 𝑗
12		cnei 21705	. . . . . . . 8 class nei
13	11, 12	cfv 6355	. . . . . . 7 class (nei‘𝑗)
14	10, 13	cfv 6355	. . . . . 6 class ((nei‘𝑗)‘{𝑥})
15	3	cv 1536	. . . . . 6 class 𝑓
16	14, 15	wss 3936	. . . . 5 wff ((nei‘𝑗)‘{𝑥}) ⊆ 𝑓
17	11	cuni 4838	. . . . . . 7 class ∪ 𝑗
18	17	cpw 4539	. . . . . 6 class 𝒫 ∪ 𝑗
19	15, 18	wss 3936	. . . . 5 wff 𝑓 ⊆ 𝒫 ∪ 𝑗
20	16, 19	wa 398	. . . 4 wff (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)
21	20, 8, 17	crab 3142	. . 3 class {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)}
22	2, 3, 4, 7, 21	cmpo 7158	. 2 class (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})
23	1, 22	wceq 1537	1 wff fLim = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})

This definition is referenced by:  flimval  22571  elflim2  22572