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

Metamath Proof Explorer

Theorem fmfg

Description: The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis elfm2.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion fmfg ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 elfm2.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
2 1 elfm2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
3 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
4 1 3 eqeltrid ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
5 filfbas ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
6 4 5 syl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
7 elfm ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
8 6 7 syl3an2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
9 2 8 bitr4d ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
10 9 eqrdv ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )