| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-fun |
|- ( Fun F <-> ( Rel F /\ ( F o. `' F ) C_ _I ) ) |
| 2 |
1
|
simprbi |
|- ( Fun F -> ( F o. `' F ) C_ _I ) |
| 3 |
|
iss |
|- ( ( F o. `' F ) C_ _I <-> ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) ) |
| 4 |
|
dfdm4 |
|- dom F = ran `' F |
| 5 |
|
dmcoeq |
|- ( dom F = ran `' F -> dom ( F o. `' F ) = dom `' F ) |
| 6 |
4 5
|
ax-mp |
|- dom ( F o. `' F ) = dom `' F |
| 7 |
|
df-rn |
|- ran F = dom `' F |
| 8 |
6 7
|
eqtr4i |
|- dom ( F o. `' F ) = ran F |
| 9 |
8
|
reseq2i |
|- ( _I |` dom ( F o. `' F ) ) = ( _I |` ran F ) |
| 10 |
9
|
eqeq2i |
|- ( ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) <-> ( F o. `' F ) = ( _I |` ran F ) ) |
| 11 |
3 10
|
bitri |
|- ( ( F o. `' F ) C_ _I <-> ( F o. `' F ) = ( _I |` ran F ) ) |
| 12 |
2 11
|
sylib |
|- ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) ) |