| 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 |
6
|
adantr |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) ) |
| 8 |
|
oveq12 |
|- ( ( y = Y /\ x = X ) -> ( y ^m x ) = ( Y ^m X ) ) |
| 9 |
8
|
ancoms |
|- ( ( x = X /\ y = Y ) -> ( y ^m x ) = ( Y ^m X ) ) |
| 10 |
9
|
reseq2d |
|- ( ( x = X /\ y = Y ) -> ( _I |` ( y ^m x ) ) = ( _I |` ( Y ^m X ) ) ) |
| 11 |
10
|
adantl |
|- ( ( ( ph /\ ( X e. C /\ Y e. C ) ) /\ ( x = X /\ y = Y ) ) -> ( _I |` ( y ^m x ) ) = ( _I |` ( Y ^m X ) ) ) |
| 12 |
|
simprl |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> X e. C ) |
| 13 |
|
simprr |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> Y e. C ) |
| 14 |
|
ovexd |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Y ^m X ) e. _V ) |
| 15 |
14
|
resiexd |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( _I |` ( Y ^m X ) ) e. _V ) |
| 16 |
7 11 12 13 15
|
ovmpod |
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) ) |