Theorem imafi2

Description: The image by a finite set is finite. See also imafi . (Contributed by Thierry Arnoux, 25-Apr-2020)

	Ref	Expression
Assertion	imafi2	⊢ ( 𝐴 ∈ Fin → ( 𝐴 “ 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )
2		resss	⊢ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴
3		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ↾ 𝐵 ) ∈ Fin )
4	2 3	mpan2	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ↾ 𝐵 ) ∈ Fin )
5		rnfi	⊢ ( ( 𝐴 ↾ 𝐵 ) ∈ Fin → ran ( 𝐴 ↾ 𝐵 ) ∈ Fin )
6	4 5	syl	⊢ ( 𝐴 ∈ Fin → ran ( 𝐴 ↾ 𝐵 ) ∈ Fin )
7	1 6	eqeltrid	⊢ ( 𝐴 ∈ Fin → ( 𝐴 “ 𝐵 ) ∈ Fin )