| Step |
Hyp |
Ref |
Expression |
| 1 |
|
resima |
|- ( ( `' F |` ( F " C ) ) " ( F " C ) ) = ( `' F " ( F " C ) ) |
| 2 |
|
df-f1 |
|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) ) |
| 3 |
2
|
simprbi |
|- ( F : A -1-1-> B -> Fun `' F ) |
| 4 |
3
|
adantr |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> Fun `' F ) |
| 5 |
|
funcnvres |
|- ( Fun `' F -> `' ( F |` C ) = ( `' F |` ( F " C ) ) ) |
| 6 |
4 5
|
syl |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> `' ( F |` C ) = ( `' F |` ( F " C ) ) ) |
| 7 |
6
|
imaeq1d |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' ( F |` C ) " ( F " C ) ) = ( ( `' F |` ( F " C ) ) " ( F " C ) ) ) |
| 8 |
|
f1ores |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) ) |
| 9 |
|
f1ocnv |
|- ( ( F |` C ) : C -1-1-onto-> ( F " C ) -> `' ( F |` C ) : ( F " C ) -1-1-onto-> C ) |
| 10 |
8 9
|
syl |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> `' ( F |` C ) : ( F " C ) -1-1-onto-> C ) |
| 11 |
|
imadmrn |
|- ( `' ( F |` C ) " dom `' ( F |` C ) ) = ran `' ( F |` C ) |
| 12 |
|
f1odm |
|- ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> dom `' ( F |` C ) = ( F " C ) ) |
| 13 |
12
|
imaeq2d |
|- ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ( `' ( F |` C ) " dom `' ( F |` C ) ) = ( `' ( F |` C ) " ( F " C ) ) ) |
| 14 |
|
f1ofo |
|- ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> `' ( F |` C ) : ( F " C ) -onto-> C ) |
| 15 |
|
forn |
|- ( `' ( F |` C ) : ( F " C ) -onto-> C -> ran `' ( F |` C ) = C ) |
| 16 |
14 15
|
syl |
|- ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ran `' ( F |` C ) = C ) |
| 17 |
11 13 16
|
3eqtr3a |
|- ( `' ( F |` C ) : ( F " C ) -1-1-onto-> C -> ( `' ( F |` C ) " ( F " C ) ) = C ) |
| 18 |
10 17
|
syl |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' ( F |` C ) " ( F " C ) ) = C ) |
| 19 |
7 18
|
eqtr3d |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( ( `' F |` ( F " C ) ) " ( F " C ) ) = C ) |
| 20 |
1 19
|
eqtr3id |
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( `' F " ( F " C ) ) = C ) |