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 
|- ( F e. ( Fil ` X ) -> ( ( X FilMap ( _I |` X ) ) ` F ) = F )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 f1oi 
 |-  ( _I |` X ) : X -1-1-onto-> X
3 f1ofo 
 |-  ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X -onto-> X )
4 2 3 ax-mp 
 |-  ( _I |` X ) : X -onto-> X
5 eqid 
 |-  ( X filGen F ) = ( X filGen F )
6 5 elfm3 
 |-  ( ( F e. ( fBas ` X ) /\ ( _I |` X ) : X -onto-> X ) -> ( t e. ( ( X FilMap ( _I |` X ) ) ` F ) <-> E. s e. ( X filGen F ) t = ( ( _I |` X ) " s ) ) )
7 1 4 6 sylancl 
 |-  ( F e. ( Fil ` X ) -> ( t e. ( ( X FilMap ( _I |` X ) ) ` F ) <-> E. s e. ( X filGen F ) t = ( ( _I |` X ) " s ) ) )
8 fgfil 
 |-  ( F e. ( Fil ` X ) -> ( X filGen F ) = F )
9 8 rexeqdv 
 |-  ( F e. ( Fil ` X ) -> ( E. s e. ( X filGen F ) t = ( ( _I |` X ) " s ) <-> E. s e. F t = ( ( _I |` X ) " s ) ) )
10 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> s C_ X )
11 resiima 
 |-  ( s C_ X -> ( ( _I |` X ) " s ) = s )
12 10 11 syl 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> ( ( _I |` X ) " s ) = s )
13 12 eqeq2d 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> ( t = ( ( _I |` X ) " s ) <-> t = s ) )
14 equcom 
 |-  ( s = t <-> t = s )
15 13 14 bitr4di 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> ( t = ( ( _I |` X ) " s ) <-> s = t ) )
16 15 rexbidva 
 |-  ( F e. ( Fil ` X ) -> ( E. s e. F t = ( ( _I |` X ) " s ) <-> E. s e. F s = t ) )
17 risset 
 |-  ( t e. F <-> E. s e. F s = t )
18 16 17 bitr4di 
 |-  ( F e. ( Fil ` X ) -> ( E. s e. F t = ( ( _I |` X ) " s ) <-> t e. F ) )
19 7 9 18 3bitrd 
 |-  ( F e. ( Fil ` X ) -> ( t e. ( ( X FilMap ( _I |` X ) ) ` F ) <-> t e. F ) )
20 19 eqrdv 
 |-  ( F e. ( Fil ` X ) -> ( ( X FilMap ( _I |` X ) ) ` F ) = F )