Metamath Proof Explorer

Theorem fmfil

Description: A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion fmfil 
|- ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 fmval 
 |-  ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( X filGen ran ( y e. B |-> ( F " y ) ) ) )
2 eqid 
 |-  ran ( y e. B |-> ( F " y ) ) = ran ( y e. B |-> ( F " y ) )
3 2 fbasrn 
 |-  ( ( B e. ( fBas ` Y ) /\ F : Y --> X /\ X e. A ) -> ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) )
4 3 3comr 
 |-  ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) )
5 fgcl 
 |-  ( ran ( y e. B |-> ( F " y ) ) e. ( fBas ` X ) -> ( X filGen ran ( y e. B |-> ( F " y ) ) ) e. ( Fil ` X ) )
6 4 5 syl 
 |-  ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( X filGen ran ( y e. B |-> ( F " y ) ) ) e. ( Fil ` X ) )
7 1 6 eqeltrd 
 |-  ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) e. ( Fil ` X ) )