Metamath Proof Explorer


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=xBC
Assertion rnmptfi BFinranAFin

Proof

Step Hyp Ref Expression
1 rnmptfi.a A=xBC
2 mptfi BFinxBCFin
3 1 2 eqeltrid BFinAFin
4 rnfi AFinranAFin
5 3 4 syl BFinranAFin