Definition df-fg

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfg	⊢ filGen
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cfbas	⊢ fBas
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( fBas ‘ 𝑤 )
7		vy	⊢ 𝑦
8	5	cpw	⊢ 𝒫 𝑤
9	3	cv	⊢ 𝑥
10	7	cv	⊢ 𝑦
11	10	cpw	⊢ 𝒫 𝑦
12	9 11	cin	⊢ ( 𝑥 ∩ 𝒫 𝑦 )
13		c0	⊢ ∅
14	12 13	wne	⊢ ( 𝑥 ∩ 𝒫 𝑦 ) ≠ ∅
15	14 7 8	crab	⊢ { 𝑦 ∈ 𝒫 𝑤 ∣ ( 𝑥 ∩ 𝒫 𝑦 ) ≠ ∅ }
16	1 3 2 6 15	cmpo	⊢ ( 𝑤 ∈ V , 𝑥 ∈ ( fBas ‘ 𝑤 ) ↦ { 𝑦 ∈ 𝒫 𝑤 ∣ ( 𝑥 ∩ 𝒫 𝑦 ) ≠ ∅ } )
17	0 16	wceq	⊢ filGen = ( 𝑤 ∈ V , 𝑥 ∈ ( fBas ‘ 𝑤 ) ↦ { 𝑦 ∈ 𝒫 𝑤 ∣ ( 𝑥 ∩ 𝒫 𝑦 ) ≠ ∅ } )