Step |
Hyp |
Ref |
Expression |
1 |
|
estrccat.c |
|- C = ( ExtStrCat ` U ) |
2 |
|
estrcid.o |
|- .1. = ( Id ` C ) |
3 |
|
estrcid.u |
|- ( ph -> U e. V ) |
4 |
|
estrcid.x |
|- ( ph -> X e. U ) |
5 |
1
|
estrccatid |
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) ) |
6 |
3 5
|
syl |
|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) ) |
7 |
6
|
simprd |
|- ( ph -> ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) |
8 |
2 7
|
eqtrid |
|- ( ph -> .1. = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) |
9 |
|
fveq2 |
|- ( x = X -> ( Base ` x ) = ( Base ` X ) ) |
10 |
9
|
reseq2d |
|- ( x = X -> ( _I |` ( Base ` x ) ) = ( _I |` ( Base ` X ) ) ) |
11 |
10
|
adantl |
|- ( ( ph /\ x = X ) -> ( _I |` ( Base ` x ) ) = ( _I |` ( Base ` X ) ) ) |
12 |
|
fvexd |
|- ( ph -> ( Base ` X ) e. _V ) |
13 |
12
|
resiexd |
|- ( ph -> ( _I |` ( Base ` X ) ) e. _V ) |
14 |
8 11 4 13
|
fvmptd |
|- ( ph -> ( .1. ` X ) = ( _I |` ( Base ` X ) ) ) |