Definition df-fg 14105

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 14096	. 2 class filGen
2		vw	. . 3 setvar w
3		vx	. . 3 setvar x
4		cvv 2763	. . 3 class _V
5	2	cv 1363	. . . 4 class w
6		cfbas 14095	. . . 4 class fBas
7	5, 6	cfv 5258	. . 3 class ( fBas ` w )
8	3	cv 1363	. . . . . 6 class x
9		vy	. . . . . . . 8 setvar y
10	9	cv 1363	. . . . . . 7 class y
11	10	cpw 3605	. . . . . 6 class ~P y
12	8, 11	cin 3156	. . . . 5 class ( x i^i ~P y )
13		c0 3450	. . . . 5 class (/)
14	12, 13	wne 2367	. . . 4 wff ( x i^i ~P y ) =/= (/)
15	5	cpw 3605	. . . 4 class ~P w
16	14, 9, 15	crab 2479	. . 3 class { y e. ~P w | ( x i^i ~P y ) =/= (/) }
17	2, 3, 4, 7, 16	cmpo 5924	. 2 class ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
18	1, 17	wceq 1364	1 wff filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )

This definition is referenced by:  metuex  14111