This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fmval ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
2 eqid ⊢ ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) )
3 2 fbasrn ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑋 ∈ 𝐴 ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
4 3 3comr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) )
5 fgcl ⊢ ( ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) ∈ ( Fil ‘ 𝑋 ) )
6 4 5 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) ∈ ( Fil ‘ 𝑋 ) )
7 1 6 eqeltrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )