Theorem rnfi

Description: The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	rnfi	$$⊢A\in \mathrm{Fin}\to \mathrm{ran}A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
2		cnvfi	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{Fin}$$
3		dmfi	$$⊢A^{-1}\in \mathrm{Fin}\to \mathrm{dom}{A}^{-1}\in \mathrm{Fin}$$
4	2 3	syl	$$⊢A\in \mathrm{Fin}\to \mathrm{dom}{A}^{-1}\in \mathrm{Fin}$$
5	1 4	eqeltrid	$$⊢A\in \mathrm{Fin}\to \mathrm{ran}A\in \mathrm{Fin}$$