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

Metamath Proof Explorer

Theorem imaelfm

Description: An image of a filter element is in the image filter. (Contributed by Jeff Hankins, 5-Oct-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis imaelfm.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion imaelfm ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐹 “ 𝑆 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imaelfm.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
2 fimass ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝐹 “ 𝑆 ) ⊆ 𝑋 )
3 2 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐹 “ 𝑆 ) ⊆ 𝑋 )
4 ssid ⊢ ( 𝐹 “ 𝑆 ) ⊆ ( 𝐹 “ 𝑆 )
5 imaeq2 ⊢ ( 𝑥 = 𝑆 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑆 ) )
6 5 sseq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) ↔ ( 𝐹 “ 𝑆 ) ⊆ ( 𝐹 “ 𝑆 ) ) )
7 6 rspcev ⊢ ( ( 𝑆 ∈ 𝐿 ∧ ( 𝐹 “ 𝑆 ) ⊆ ( 𝐹 “ 𝑆 ) ) → ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) )
8 4 7 mpan2 ⊢ ( 𝑆 ∈ 𝐿 → ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) )
9 3 8 anim12i ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑆 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑆 ) ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) ) )
10 1 elfm2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐹 “ 𝑆 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( ( 𝐹 “ 𝑆 ) ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) ) ) )
11 10 adantr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑆 ∈ 𝐿 ) → ( ( 𝐹 “ 𝑆 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( ( 𝐹 “ 𝑆 ) ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐿 ( 𝐹 “ 𝑥 ) ⊆ ( 𝐹 “ 𝑆 ) ) ) )
12 9 11 mpbird ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐹 “ 𝑆 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )