Definition df-fg 20361

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 20352	. 2 class filGen
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 3408	. . 3 class V
5	2	cv 1542	. . . 4 class 𝑤
6		cfbas 20351	. . . 4 class fBas
7	5, 6	cfv 6380	. . 3 class (fBas‘𝑤)
8	3	cv 1542	. . . . . 6 class 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1542	. . . . . . 7 class 𝑦
11	10	cpw 4513	. . . . . 6 class 𝒫 𝑦
12	8, 11	cin 3865	. . . . 5 class (𝑥 ∩ 𝒫 𝑦)
13		c0 4237	. . . . 5 class ∅
14	12, 13	wne 2940	. . . 4 wff (𝑥 ∩ 𝒫 𝑦) ≠ ∅
15	5	cpw 4513	. . . 4 class 𝒫 𝑤
16	14, 9, 15	crab 3065	. . 3 class {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}
17	2, 3, 4, 7, 16	cmpo 7215	. 2 class (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
18	1, 17	wceq 1543	1 wff filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})

This definition is referenced by:  fgval  22767  fgabs  22776