Theorem f1resf1

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

	Ref	Expression
Assertion	f1resf1	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F |` C ) : C --> D ) -> ( F |` C ) : C -1-1-> D )

Proof

Step	Hyp	Ref	Expression
1		f1ssres	|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-> B )
2	1	3adant3	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F |` C ) : C --> D ) -> ( F |` C ) : C -1-1-> B )
3		frn	|- ( ( F |` C ) : C --> D -> ran ( F |` C ) C_ D )
4	3	3ad2ant3	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F |` C ) : C --> D ) -> ran ( F |` C ) C_ D )
5		f1ssr	|- ( ( ( F |` C ) : C -1-1-> B /\ ran ( F |` C ) C_ D ) -> ( F |` C ) : C -1-1-> D )
6	2 4 5	syl2anc	|- ( ( F : A -1-1-> B /\ C C_ A /\ ( F |` C ) : C --> D ) -> ( F |` C ) : C -1-1-> D )