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

Proof

Step Hyp Ref Expression
1 f1f ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴𝐵 )
2 1 frnd ( 𝐹 : 𝐴1-1𝐵 → ran 𝐹𝐵 )
3 ssfi ( ( 𝐵 ∈ Fin ∧ ran 𝐹𝐵 ) → ran 𝐹 ∈ Fin )
4 2 3 sylan2 ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴1-1𝐵 ) → ran 𝐹 ∈ Fin )
5 f1f1orn ( 𝐹 : 𝐴1-1𝐵𝐹 : 𝐴1-1-onto→ ran 𝐹 )
6 5 adantl ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : 𝐴1-1-onto→ ran 𝐹 )
7 f1ocnv ( 𝐹 : 𝐴1-1-onto→ ran 𝐹 𝐹 : ran 𝐹1-1-onto𝐴 )
8 f1ofo ( 𝐹 : ran 𝐹1-1-onto𝐴 𝐹 : ran 𝐹onto𝐴 )
9 6 7 8 3syl ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐹 : ran 𝐹onto𝐴 )
10 fofi ( ( ran 𝐹 ∈ Fin ∧ 𝐹 : ran 𝐹onto𝐴 ) → 𝐴 ∈ Fin )
11 4 9 10 syl2anc ( ( 𝐵 ∈ Fin ∧ 𝐹 : 𝐴1-1𝐵 ) → 𝐴 ∈ Fin )