Metamath Proof Explorer


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=wV,xfBaswy𝒫w|x𝒫y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfg classfilGen
1 vw setvarw
2 cvv classV
3 vx setvarx
4 cfbas classfBas
5 1 cv setvarw
6 5 4 cfv classfBasw
7 vy setvary
8 5 cpw class𝒫w
9 3 cv setvarx
10 7 cv setvary
11 10 cpw class𝒫y
12 9 11 cin classx𝒫y
13 c0 class
14 12 13 wne wffx𝒫y
15 14 7 8 crab classy𝒫w|x𝒫y
16 1 3 2 6 15 cmpo classwV,xfBaswy𝒫w|x𝒫y
17 0 16 wceq wfffilGen=wV,xfBaswy𝒫w|x𝒫y