Theorem rnfi

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

	Ref	Expression
Assertion	rnfi	⊢ ( 𝐴 ∈ Fin → ran 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
2		cnvfi	⊢ ( 𝐴 ∈ Fin → ◡ 𝐴 ∈ Fin )
3		dmfi	⊢ ( ◡ 𝐴 ∈ Fin → dom ◡ 𝐴 ∈ Fin )
4	2 3	syl	⊢ ( 𝐴 ∈ Fin → dom ◡ 𝐴 ∈ Fin )
5	1 4	eqeltrid	⊢ ( 𝐴 ∈ Fin → ran 𝐴 ∈ Fin )