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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfg | |
|
1 | vw | |
|
2 | cvv | |
|
3 | vx | |
|
4 | cfbas | |
|
5 | 1 | cv | |
6 | 5 4 | cfv | |
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 | |
17 | 0 16 | wceq | |