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	$$⊢\left(A\in \mathrm{Fin}\wedge F:A\underset{onto}{⟶}B\right)\to B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		fodomfi	$$⊢\left(A\in \mathrm{Fin}\wedge F:A\underset{onto}{⟶}B\right)\to B\preccurlyeq A$$
2		domfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\preccurlyeq A\right)\to B\in \mathrm{Fin}$$
3	1 2	syldan	$$⊢\left(A\in \mathrm{Fin}\wedge F:A\underset{onto}{⟶}B\right)\to B\in \mathrm{Fin}$$