Metamath Proof Explorer


Theorem oasuc

Description: Addition with successor. Definition 8.1 of TakeutiZaring p. 56. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oasuc
|- ( ( A e. On /\ B e. On ) -> ( A +o suc B ) = suc ( A +o B ) )

Proof

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