Step |
Hyp |
Ref |
Expression |
1 |
|
limom |
|- Lim _om |
2 |
|
frsuc |
|- ( B e. _om -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) |` _om ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) |` _om ) ` B ) ) ) |
3 |
|
peano2 |
|- ( B e. _om -> suc B e. _om ) |
4 |
3
|
fvresd |
|- ( B e. _om -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) |` _om ) ` suc B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) ) |
5 |
|
fvres |
|- ( B e. _om -> ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) |` _om ) ` B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) |
6 |
5
|
fveq2d |
|- ( B e. _om -> ( ( x e. _V |-> ( x .o A ) ) ` ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) |` _om ) ` B ) ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) ) |
7 |
2 4 6
|
3eqtr3d |
|- ( B e. _om -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) ) |
8 |
1 7
|
oesuclem |
|- ( ( A e. On /\ B e. _om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) ) |