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 )