Theorem rnmptfi

Description: The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	rnmptfi.a	$$⊢A=\left(x\in B⟼C\right)$$
Assertion	rnmptfi	$$⊢B\in \mathrm{Fin}\to \mathrm{ran}A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		rnmptfi.a	$$⊢A=\left(x\in B⟼C\right)$$
2		mptfi	$$⊢B\in \mathrm{Fin}\to \left(x\in B⟼C\right)\in \mathrm{Fin}$$
3	1 2	eqeltrid	$$⊢B\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
4		rnfi	$$⊢A\in \mathrm{Fin}\to \mathrm{ran}A\in \mathrm{Fin}$$
5	3 4	syl	$$⊢B\in \mathrm{Fin}\to \mathrm{ran}A\in \mathrm{Fin}$$