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 \in Fin \land F : A \underset{1-1}{⟶} B) \to A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2	1	frnd	$⊢ F : A \underset{1-1}{⟶} B \to ran F \subseteq B$
3		ssfi	$⊢ (B \in Fin \land ran F \subseteq B) \to ran F \in Fin$
4	2 3	sylan2	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to ran F \in Fin$
5		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
6	5	adantl	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1 onto}{⟶} ran F$
7		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} ran F \to F^{-1} : ran F \underset{1-1 onto}{⟶} A$
8		f1ofo	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} A \to F^{-1} : ran F \underset{onto}{⟶} A$
9	6 7 8	3syl	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to F^{-1} : ran F \underset{onto}{⟶} A$
10		fofi	$⊢ (ran F \in Fin \land F^{-1} : ran F \underset{onto}{⟶} A) \to A \in Fin$
11	4 9 10	syl2anc	$⊢ (B \in Fin \land F : A \underset{1-1}{⟶} B) \to A \in Fin$