Metamath Proof Explorer


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 )