Step |
Hyp |
Ref |
Expression |
1 |
|
dfrtrcl3 |
|- t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) |
2 |
|
df-n0 |
|- NN0 = ( NN u. { 0 } ) |
3 |
2
|
equncomi |
|- NN0 = ( { 0 } u. NN ) |
4 |
|
iuneq1 |
|- ( NN0 = ( { 0 } u. NN ) -> U_ n e. NN0 ( r ^r n ) = U_ n e. ( { 0 } u. NN ) ( r ^r n ) ) |
5 |
3 4
|
ax-mp |
|- U_ n e. NN0 ( r ^r n ) = U_ n e. ( { 0 } u. NN ) ( r ^r n ) |
6 |
|
iunxun |
|- U_ n e. ( { 0 } u. NN ) ( r ^r n ) = ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) ) |
7 |
5 6
|
eqtri |
|- U_ n e. NN0 ( r ^r n ) = ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) ) |
8 |
|
c0ex |
|- 0 e. _V |
9 |
|
oveq2 |
|- ( n = 0 -> ( r ^r n ) = ( r ^r 0 ) ) |
10 |
8 9
|
iunxsn |
|- U_ n e. { 0 } ( r ^r n ) = ( r ^r 0 ) |
11 |
10
|
a1i |
|- ( r e. _V -> U_ n e. { 0 } ( r ^r n ) = ( r ^r 0 ) ) |
12 |
|
oveq1 |
|- ( x = r -> ( x ^r n ) = ( r ^r n ) ) |
13 |
12
|
iuneq2d |
|- ( x = r -> U_ n e. NN ( x ^r n ) = U_ n e. NN ( r ^r n ) ) |
14 |
|
dftrcl3 |
|- t+ = ( x e. _V |-> U_ n e. NN ( x ^r n ) ) |
15 |
|
nnex |
|- NN e. _V |
16 |
|
ovex |
|- ( r ^r n ) e. _V |
17 |
15 16
|
iunex |
|- U_ n e. NN ( r ^r n ) e. _V |
18 |
13 14 17
|
fvmpt |
|- ( r e. _V -> ( t+ ` r ) = U_ n e. NN ( r ^r n ) ) |
19 |
18
|
eqcomd |
|- ( r e. _V -> U_ n e. NN ( r ^r n ) = ( t+ ` r ) ) |
20 |
11 19
|
uneq12d |
|- ( r e. _V -> ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) ) = ( ( r ^r 0 ) u. ( t+ ` r ) ) ) |
21 |
7 20
|
syl5eq |
|- ( r e. _V -> U_ n e. NN0 ( r ^r n ) = ( ( r ^r 0 ) u. ( t+ ` r ) ) ) |
22 |
21
|
mpteq2ia |
|- ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) ) |
23 |
1 22
|
eqtri |
|- t* = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) ) |