Step |
Hyp |
Ref |
Expression |
1 |
|
inpreima |
|- ( Fun F -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) ) |
2 |
|
funforn |
|- ( Fun F <-> F : dom F -onto-> ran F ) |
3 |
|
fof |
|- ( F : dom F -onto-> ran F -> F : dom F --> ran F ) |
4 |
2 3
|
sylbi |
|- ( Fun F -> F : dom F --> ran F ) |
5 |
|
fimacnv |
|- ( F : dom F --> ran F -> ( `' F " ran F ) = dom F ) |
6 |
4 5
|
syl |
|- ( Fun F -> ( `' F " ran F ) = dom F ) |
7 |
6
|
ineq2d |
|- ( Fun F -> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( ( `' F " A ) i^i dom F ) ) |
8 |
|
cnvresima |
|- ( `' ( F |` dom F ) " A ) = ( ( `' F " A ) i^i dom F ) |
9 |
|
resdm2 |
|- ( F |` dom F ) = `' `' F |
10 |
|
funrel |
|- ( Fun F -> Rel F ) |
11 |
|
dfrel2 |
|- ( Rel F <-> `' `' F = F ) |
12 |
10 11
|
sylib |
|- ( Fun F -> `' `' F = F ) |
13 |
9 12
|
eqtrid |
|- ( Fun F -> ( F |` dom F ) = F ) |
14 |
13
|
cnveqd |
|- ( Fun F -> `' ( F |` dom F ) = `' F ) |
15 |
14
|
imaeq1d |
|- ( Fun F -> ( `' ( F |` dom F ) " A ) = ( `' F " A ) ) |
16 |
8 15
|
eqtr3id |
|- ( Fun F -> ( ( `' F " A ) i^i dom F ) = ( `' F " A ) ) |
17 |
1 7 16
|
3eqtrrd |
|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) ) |