Metamath Proof Explorer

Theorem rnfi

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

Ref Expression
Assertion rnfi 
|- ( A e. Fin -> ran A e. Fin )

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran A = dom `' A
2 cnvfi 
 |-  ( A e. Fin -> `' A e. Fin )
3 dmfi 
 |-  ( `' A e. Fin -> dom `' A e. Fin )
4 2 3 syl 
 |-  ( A e. Fin -> dom `' A e. Fin )
5 1 4 eqeltrid 
 |-  ( A e. Fin -> ran A e. Fin )