Step |
Hyp |
Ref |
Expression |
1 |
|
rdgsuc |
|- ( B e. On -> ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) ) |
2 |
1
|
adantl |
|- ( ( A e. On /\ B e. On ) -> ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) ) |
3 |
|
suceloni |
|- ( B e. On -> suc B e. On ) |
4 |
|
omv |
|- ( ( A e. On /\ suc B e. On ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) ) |
5 |
3 4
|
sylan2 |
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) ) |
6 |
|
ovex |
|- ( A .o B ) e. _V |
7 |
|
oveq1 |
|- ( x = ( A .o B ) -> ( x +o A ) = ( ( A .o B ) +o A ) ) |
8 |
|
eqid |
|- ( x e. _V |-> ( x +o A ) ) = ( x e. _V |-> ( x +o A ) ) |
9 |
|
ovex |
|- ( ( A .o B ) +o A ) e. _V |
10 |
7 8 9
|
fvmpt |
|- ( ( A .o B ) e. _V -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A ) ) |
11 |
6 10
|
ax-mp |
|- ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A ) |
12 |
|
omv |
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) |
13 |
12
|
fveq2d |
|- ( ( A e. On /\ B e. On ) -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) ) |
14 |
11 13
|
eqtr3id |
|- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) +o A ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) ) |
15 |
2 5 14
|
3eqtr4d |
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) ) |