This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Fin \to ran A \in Fin$

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