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 Fin F : A 1-1 B A 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 B
3 ssfi B Fin ran F B ran F Fin
4 2 3 sylan2 B Fin F : A 1-1 B ran F Fin
5 f1f1orn F : A 1-1 B F : A 1-1 onto ran F
6 5 adantl B Fin F : A 1-1 B F : A 1-1 onto ran F
7 f1ocnv F : A 1-1 onto ran F F -1 : ran F 1-1 onto A
8 f1ofo F -1 : ran F 1-1 onto A F -1 : ran F onto A
9 6 7 8 3syl B Fin F : A 1-1 B F -1 : ran F onto A
10 fofi ran F Fin F -1 : ran F onto A A Fin
11 4 9 10 syl2anc B Fin F : A 1-1 B A Fin