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