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 ( ( 𝐵 ∈ 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 )