f1ssres

Description: A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015)

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

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

Metamath Proof Explorer