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 e. Fin /\ F : A -onto-> B ) -> B e. Fin )

Proof

Step Hyp Ref Expression
1 fodomfi 
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A )
2 domfi 
 |-  ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin )
3 1 2 syldan 
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> B e. Fin )