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\in \mathrm{Fin}\to A\left[B\right]\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢A\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
2		resss	$$⊢{A\upharpoonright }_B\subseteq A$$
3		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge {A\upharpoonright }_B\subseteq A\right)\to {A\upharpoonright }_B\in \mathrm{Fin}$$
4	2 3	mpan2	$$⊢A\in \mathrm{Fin}\to {A\upharpoonright }_B\in \mathrm{Fin}$$
5		rnfi	$$⊢{A\upharpoonright }_B\in \mathrm{Fin}\to \mathrm{ran}\left({A\upharpoonright }_B\right)\in \mathrm{Fin}$$
6	4 5	syl	$$⊢A\in \mathrm{Fin}\to \mathrm{ran}\left({A\upharpoonright }_B\right)\in \mathrm{Fin}$$
7	1 6	eqeltrid	$$⊢A\in \mathrm{Fin}\to A\left[B\right]\in \mathrm{Fin}$$