Definition df-fg 16655

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

Distinct variable group:   x, y, w

Detailed syntax breakdown of Definition df-fg

Step	Hyp	Ref	Expression
1		cfg 16645	. 2 class filGen
2		vw	. . 3 set w
3		vx	. . 3 set x
4		cvv 2916	. . 3 class _V
5	2	cv 1648	. . . 4 class w
6		cfbas 16644	. . . 4 class fBas
7	5, 6	cfv 5413	. . 3 class ( fBas ` w )
8	3	cv 1648	. . . . . 6 class x
9		vy	. . . . . . . 8 set y
10	9	cv 1648	. . . . . . 7 class y
11	10	cpw 3759	. . . . . 6 class ~P y
12	8, 11	cin 3279	. . . . 5 class ( x i^i ~P y )
13		c0 3588	. . . . 5 class (/)
14	12, 13	wne 2567	. . . 4 wff ( x i^i ~P y ) =/= (/)
15	5	cpw 3759	. . . 4 class ~P w
16	14, 9, 15	crab 2670	. . 3 class { y e. ~P w | ( x i^i ~P y ) =/= (/) }
17	2, 3, 4, 7, 16	cmpt2 6042	. 2 class ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
18	1, 17	wceq 1649	1 wff filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )

This definition is referenced by:  fgval  17855  fgabs  17864