| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcestrcsetc.e |
|- E = ( ExtStrCat ` U ) |
| 2 |
|
funcestrcsetc.s |
|- S = ( SetCat ` U ) |
| 3 |
|
funcestrcsetc.b |
|- B = ( Base ` E ) |
| 4 |
|
funcestrcsetc.c |
|- C = ( Base ` S ) |
| 5 |
|
funcestrcsetc.u |
|- ( ph -> U e. WUni ) |
| 6 |
|
funcestrcsetc.f |
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
| 7 |
|
funcestrcsetc.g |
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) ) |
| 8 |
|
eqid |
|- ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) |
| 9 |
|
ovex |
|- ( ( Base ` y ) ^m ( Base ` x ) ) e. _V |
| 10 |
|
resiexg |
|- ( ( ( Base ` y ) ^m ( Base ` x ) ) e. _V -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V ) |
| 11 |
9 10
|
ax-mp |
|- ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V |
| 12 |
8 11
|
fnmpoi |
|- ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) Fn ( B X. B ) |
| 13 |
7
|
fneq1d |
|- ( ph -> ( G Fn ( B X. B ) <-> ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) Fn ( B X. B ) ) ) |
| 14 |
12 13
|
mpbiri |
|- ( ph -> G Fn ( B X. B ) ) |