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 → X FilMap F ⁡ B ∈ Fil ⁡ X

Proof

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