Description: The filter map applied to the identity. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Mario Carneiro, 27-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fmid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | filfbas | |
|
2 | f1oi | |
|
3 | f1ofo | |
|
4 | 2 3 | ax-mp | |
5 | eqid | |
|
6 | 5 | elfm3 | |
7 | 1 4 6 | sylancl | |
8 | fgfil | |
|
9 | 8 | rexeqdv | |
10 | filelss | |
|
11 | resiima | |
|
12 | 10 11 | syl | |
13 | 12 | eqeq2d | |
14 | equcom | |
|
15 | 13 14 | bitr4di | |
16 | 15 | rexbidva | |
17 | risset | |
|
18 | 16 17 | bitr4di | |
19 | 7 9 18 | 3bitrd | |
20 | 19 | eqrdv | |