Definition df-fg 20508

Description: Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)

Assertion

Ref	Expression
df-fg	⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})

Distinct variable group:   𝑥,𝑦,𝑤

Detailed syntax breakdown of Definition df-fg

Step	Hyp	Ref	Expression
1		cfg 20499	. 2 class filGen
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3422	. . 3 class V
5	2	cv 1538	. . . 4 class 𝑤
6		cfbas 20498	. . . 4 class fBas
7	5, 6	cfv 6418	. . 3 class (fBas‘𝑤)
8	3	cv 1538	. . . . . 6 class 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1538	. . . . . . 7 class 𝑦
11	10	cpw 4530	. . . . . 6 class 𝒫 𝑦
12	8, 11	cin 3882	. . . . 5 class (𝑥 ∩ 𝒫 𝑦)
13		c0 4253	. . . . 5 class ∅
14	12, 13	wne 2942	. . . 4 wff (𝑥 ∩ 𝒫 𝑦) ≠ ∅
15	5	cpw 4530	. . . 4 class 𝒫 𝑤
16	14, 9, 15	crab 3067	. . 3 class {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}
17	2, 3, 4, 7, 16	cmpo 7257	. 2 class (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
18	1, 17	wceq 1539	1 wff filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})

This definition is referenced by:  fgval  22929  fgabs  22938