| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imaidfu.i |
|- I = ( idFunc ` C ) |
| 2 |
|
imaidfu.d |
|- ( ph -> I e. ( D Func E ) ) |
| 3 |
|
eqidd |
|- ( ph -> ( Base ` D ) = ( Base ` D ) ) |
| 4 |
1 2 3
|
idfu1sta |
|- ( ph -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) ) |
| 5 |
4
|
imaeq1d |
|- ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) ) |
| 6 |
|
ssid |
|- ( Base ` D ) C_ ( Base ` D ) |
| 7 |
|
resiima |
|- ( ( Base ` D ) C_ ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D ) ) |
| 8 |
6 7
|
ax-mp |
|- ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D ) |
| 9 |
5 8
|
eqtrdi |
|- ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) ) |