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 ) )