f1ssr

Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015)

		Ref	Expression
	Assertion	f1ssr	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to F : A \underset{1-1}{⟶} C$

Step	Hyp	Ref	Expression
1		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
2	1	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to F Fn A$
3		simpr	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to ran F \subseteq C$
4		df-f	$⊢ F : A ⟶ C \leftrightarrow (F Fn A \land ran F \subseteq C)$
5	2 3 4	sylanbrc	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to F : A ⟶ C$
6		df-f1	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land Fun F^{-1})$
7	6	simprbi	$⊢ F : A \underset{1-1}{⟶} B \to Fun F^{-1}$
8	7	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to Fun F^{-1}$
9		df-f1	$⊢ F : A \underset{1-1}{⟶} C \leftrightarrow (F : A ⟶ C \land Fun F^{-1})$
10	5 8 9	sylanbrc	$⊢ (F : A \underset{1-1}{⟶} B \land ran F \subseteq C) \to F : A \underset{1-1}{⟶} C$

Metamath Proof Explorer