Metamath Proof Explorer


Theorem fmid

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 FFilXXFilMapIXF=F

Proof

Step Hyp Ref Expression
1 filfbas FFilXFfBasX
2 f1oi IX:X1-1 ontoX
3 f1ofo IX:X1-1 ontoXIX:XontoX
4 2 3 ax-mp IX:XontoX
5 eqid XfilGenF=XfilGenF
6 5 elfm3 FfBasXIX:XontoXtXFilMapIXFsXfilGenFt=IXs
7 1 4 6 sylancl FFilXtXFilMapIXFsXfilGenFt=IXs
8 fgfil FFilXXfilGenF=F
9 8 rexeqdv FFilXsXfilGenFt=IXssFt=IXs
10 filelss FFilXsFsX
11 resiima sXIXs=s
12 10 11 syl FFilXsFIXs=s
13 12 eqeq2d FFilXsFt=IXst=s
14 equcom s=tt=s
15 13 14 bitr4di FFilXsFt=IXss=t
16 15 rexbidva FFilXsFt=IXssFs=t
17 risset tFsFs=t
18 16 17 bitr4di FFilXsFt=IXstF
19 7 9 18 3bitrd FFilXtXFilMapIXFtF
20 19 eqrdv FFilXXFilMapIXF=F