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∈A∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B∈Fil⁡X

Proof

Step Hyp Ref Expression
1 fmval ⊢X∈A∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B=XfilGenran⁡y∈B⟼Fy
2 eqid ⊢ran⁡y∈B⟼Fy=ran⁡y∈B⟼Fy
3 2 fbasrn ⊢B∈fBas⁡Y∧F:Y⟶X∧X∈A→ran⁡y∈B⟼Fy∈fBas⁡X
4 3 3comr ⊢X∈A∧B∈fBas⁡Y∧F:Y⟶X→ran⁡y∈B⟼Fy∈fBas⁡X
5 fgcl ⊢ran⁡y∈B⟼Fy∈fBas⁡X→XfilGenran⁡y∈B⟼Fy∈Fil⁡X
6 4 5 syl ⊢X∈A∧B∈fBas⁡Y∧F:Y⟶X→XfilGenran⁡y∈B⟼Fy∈Fil⁡X
7 1 6 eqeltrd ⊢X∈A∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B∈Fil⁡X