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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		fodomfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ≼ 𝐴 )
2		domfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin )
3	1 2	syldan	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ Fin )