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 )