| 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 |
|
funcestrcsetc.m |
|- M = ( Base ` X ) |
| 9 |
|
funcestrcsetc.n |
|- N = ( Base ` Y ) |
| 10 |
7
|
adantr |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) ) |
| 11 |
|
fveq2 |
|- ( y = Y -> ( Base ` y ) = ( Base ` Y ) ) |
| 12 |
|
fveq2 |
|- ( x = X -> ( Base ` x ) = ( Base ` X ) ) |
| 13 |
11 12
|
oveqan12rd |
|- ( ( x = X /\ y = Y ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` Y ) ^m ( Base ` X ) ) ) |
| 14 |
9 8
|
oveq12i |
|- ( N ^m M ) = ( ( Base ` Y ) ^m ( Base ` X ) ) |
| 15 |
13 14
|
eqtr4di |
|- ( ( x = X /\ y = Y ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( N ^m M ) ) |
| 16 |
15
|
reseq2d |
|- ( ( x = X /\ y = Y ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( N ^m M ) ) ) |
| 17 |
16
|
adantl |
|- ( ( ( ph /\ ( X e. B /\ Y e. B ) ) /\ ( x = X /\ y = Y ) ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( N ^m M ) ) ) |
| 18 |
|
simprl |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. B ) |
| 19 |
|
simprr |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. B ) |
| 20 |
|
ovexd |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( N ^m M ) e. _V ) |
| 21 |
20
|
resiexd |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( _I |` ( N ^m M ) ) e. _V ) |
| 22 |
10 17 18 19 21
|
ovmpod |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( N ^m M ) ) ) |