| 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 |
|
eqid |
|- ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) |
| 8 |
|
ovex |
|- ( y ^m x ) e. _V |
| 9 |
|
resiexg |
|- ( ( y ^m x ) e. _V -> ( _I |` ( y ^m x ) ) e. _V ) |
| 10 |
8 9
|
ax-mp |
|- ( _I |` ( y ^m x ) ) e. _V |
| 11 |
7 10
|
fnmpoi |
|- ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) Fn ( C X. C ) |
| 12 |
6
|
fneq1d |
|- ( ph -> ( G Fn ( C X. C ) <-> ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) Fn ( C X. C ) ) ) |
| 13 |
11 12
|
mpbiri |
|- ( ph -> G Fn ( C X. C ) ) |