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 ) |