| 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 |
1 2 3 4 5 6 7 8 9
|
funcestrcsetclem5 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( N ^m M ) ) ) |
| 11 |
10
|
3adant3 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( N ^m M ) ) -> ( X G Y ) = ( _I |` ( N ^m M ) ) ) |
| 12 |
11
|
fveq1d |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( N ^m M ) ) -> ( ( X G Y ) ` H ) = ( ( _I |` ( N ^m M ) ) ` H ) ) |
| 13 |
|
fvresi |
|- ( H e. ( N ^m M ) -> ( ( _I |` ( N ^m M ) ) ` H ) = H ) |
| 14 |
13
|
3ad2ant3 |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( N ^m M ) ) -> ( ( _I |` ( N ^m M ) ) ` H ) = H ) |
| 15 |
12 14
|
eqtrd |
|- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( N ^m M ) ) -> ( ( X G Y ) ` H ) = H ) |