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

Metamath Proof Explorer

Theorem f1fi

Description: If a 1-to-1 function has a finite codomain its domain is finite. (Contributed by FL, 31-Jul-2009) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion f1fi 
|- ( ( B e. Fin /\ F : A -1-1-> B ) -> A e. Fin )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 1 frnd 
 |-  ( F : A -1-1-> B -> ran F C_ B )
3 ssfi 
 |-  ( ( B e. Fin /\ ran F C_ B ) -> ran F e. Fin )
4 2 3 sylan2 
 |-  ( ( B e. Fin /\ F : A -1-1-> B ) -> ran F e. Fin )
5 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
6 5 adantl 
 |-  ( ( B e. Fin /\ F : A -1-1-> B ) -> F : A -1-1-onto-> ran F )
7 f1ocnv 
 |-  ( F : A -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> A )
8 f1ofo 
 |-  ( `' F : ran F -1-1-onto-> A -> `' F : ran F -onto-> A )
9 6 7 8 3syl 
 |-  ( ( B e. Fin /\ F : A -1-1-> B ) -> `' F : ran F -onto-> A )
10 fofi 
 |-  ( ( ran F e. Fin /\ `' F : ran F -onto-> A ) -> A e. Fin )
11 4 9 10 syl2anc 
 |-  ( ( B e. Fin /\ F : A -1-1-> B ) -> A e. Fin )