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 = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfg	|- filGen
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4		cfbas	|- fBas
5	1	cv	|- w
6	5 4	cfv	|- ( fBas ` w )
7		vy	|- y
8	5	cpw	|- ~P w
9	3	cv	|- x
10	7	cv	|- y
11	10	cpw	|- ~P y
12	9 11	cin	|- ( x i^i ~P y )
13		c0	|- (/)
14	12 13	wne	|- ( x i^i ~P y ) =/= (/)
15	14 7 8	crab	|- { y e. ~P w | ( x i^i ~P y ) =/= (/) }
16	1 3 2 6 15	cmpo	|- ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
17	0 16	wceq	|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )