Definition df-fg 14562

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 14553	. 2 class filGen
2		vw	. . 3 setvar 𝑤
3		vx	. . 3 setvar 𝑥
4		cvv 2802	. . 3 class V
5	2	cv 1396	. . . 4 class 𝑤
6		cfbas 14552	. . . 4 class fBas
7	5, 6	cfv 5326	. . 3 class (fBas‘𝑤)
8	3	cv 1396	. . . . . 6 class 𝑥
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1396	. . . . . . 7 class 𝑦
11	10	cpw 3652	. . . . . 6 class 𝒫 𝑦
12	8, 11	cin 3199	. . . . 5 class (𝑥 ∩ 𝒫 𝑦)
13		c0 3494	. . . . 5 class ∅
14	12, 13	wne 2402	. . . 4 wff (𝑥 ∩ 𝒫 𝑦) ≠ ∅
15	5	cpw 3652	. . . 4 class 𝒫 𝑤
16	14, 9, 15	crab 2514	. . 3 class {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}
17	2, 3, 4, 7, 16	cmpo 6019	. 2 class (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
18	1, 17	wceq 1397	1 wff filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})

This definition is referenced by:  metuex  14568