f1ss

Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013)

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

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2		fss	$⊢ (F : A ⟶ B \land B \subseteq C) \to F : A ⟶ C$
3	1 2	sylan	$⊢ (F : A \underset{1-1}{⟶} B \land B \subseteq C) \to F : A ⟶ C$
4		df-f1	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land Fun F^{-1})$
5	4	simprbi	$⊢ F : A \underset{1-1}{⟶} B \to Fun F^{-1}$
6	5	adantr	$⊢ (F : A \underset{1-1}{⟶} B \land B \subseteq C) \to Fun F^{-1}$
7		df-f1	$⊢ F : A \underset{1-1}{⟶} C \leftrightarrow (F : A ⟶ C \land Fun F^{-1})$
8	3 6 7	sylanbrc	$⊢ (F : A \underset{1-1}{⟶} B \land B \subseteq C) \to F : A \underset{1-1}{⟶} C$

Metamath Proof Explorer