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	|- ( A e. Fin -> ( A " B ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( A " B ) = ran ( A |` B )
2		resss	|- ( A |` B ) C_ A
3		ssfi	|- ( ( A e. Fin /\ ( A |` B ) C_ A ) -> ( A |` B ) e. Fin )
4	2 3	mpan2	|- ( A e. Fin -> ( A |` B ) e. Fin )
5		rnfi	|- ( ( A |` B ) e. Fin -> ran ( A |` B ) e. Fin )
6	4 5	syl	|- ( A e. Fin -> ran ( A |` B ) e. Fin )
7	1 6	eqeltrid	|- ( A e. Fin -> ( A " B ) e. Fin )