f1resf1

Description: The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022)

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

Step	Hyp	Ref	Expression
1		f1ssres	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({F ↾}_{C}) : C \underset{1-1}{⟶} B$
2	1	3adant3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land ({F ↾}_{C}) : C ⟶ D) \to ({F ↾}_{C}) : C \underset{1-1}{⟶} B$
3		frn	$⊢ ({F ↾}_{C}) : C ⟶ D \to ran ({F ↾}_{C}) \subseteq D$
4	3	3ad2ant3	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land ({F ↾}_{C}) : C ⟶ D) \to ran ({F ↾}_{C}) \subseteq D$
5		f1ssr	$⊢ (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land ran ({F ↾}_{C}) \subseteq D) \to ({F ↾}_{C}) : C \underset{1-1}{⟶} D$
6	2 4 5	syl2anc	$⊢ (F : A \underset{1-1}{⟶} B \land C \subseteq A \land ({F ↾}_{C}) : C ⟶ D) \to ({F ↾}_{C}) : C \underset{1-1}{⟶} D$

Metamath Proof Explorer