This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )