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

Metamath Proof Explorer

Theorem fofi

Description: If an onto function has a finite domain, its codomain/range is finite. Theorem 37 of Suppes p. 104. (Contributed by NM, 25-Mar-2007)

		Ref	Expression
	Assertion	fofi	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B \in Fin$

Step	Hyp	Ref	Expression
1		fodomfi	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B ≼ A$
2		domfi	$⊢ (A \in Fin \land B ≼ A) \to B \in Fin$
3	1 2	syldan	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} B) \to B \in Fin$