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 = ( x e. B |-> C )
Assertion	rnmptfi	|- ( B e. Fin -> ran A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		rnmptfi.a	|- A = ( x e. B |-> C )
2		mptfi	|- ( B e. Fin -> ( x e. B |-> C ) e. Fin )
3	1 2	eqeltrid	|- ( B e. Fin -> A e. Fin )
4		rnfi	|- ( A e. Fin -> ran A e. Fin )
5	3 4	syl	|- ( B e. Fin -> ran A e. Fin )