| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcsetcestrc.s |
|- S = ( SetCat ` U ) |
| 2 |
|
funcsetcestrc.c |
|- C = ( Base ` S ) |
| 3 |
|
funcsetcestrc.f |
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) ) |
| 4 |
|
funcsetcestrc.u |
|- ( ph -> U e. WUni ) |
| 5 |
|
funcsetcestrc.o |
|- ( ph -> _om e. U ) |
| 6 |
|
funcsetcestrc.g |
|- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) ) |
| 7 |
1 2 3 4 5 6
|
funcsetcestrclem5 |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) ) |
| 8 |
7
|
3adant3 |
|- ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) ) |
| 9 |
8
|
fveq1d |
|- ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( ( X G Y ) ` H ) = ( ( _I |` ( Y ^m X ) ) ` H ) ) |
| 10 |
|
fvresi |
|- ( H e. ( Y ^m X ) -> ( ( _I |` ( Y ^m X ) ) ` H ) = H ) |
| 11 |
10
|
3ad2ant3 |
|- ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( ( _I |` ( Y ^m X ) ) ` H ) = H ) |
| 12 |
9 11
|
eqtrd |
|- ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( ( X G Y ) ` H ) = H ) |