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 𝐹 ) ‘ 𝐵 ) )