Metamath Proof Explorer

Theorem oav

Description: Value of ordinal addition. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oav 
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )

Proof

Step Hyp Ref Expression
1 rdgeq2 
 |-  ( y = A -> rec ( ( x e. _V |-> suc x ) , y ) = rec ( ( x e. _V |-> suc x ) , A ) )
2 1 fveq1d 
 |-  ( y = A -> ( rec ( ( x e. _V |-> suc x ) , y ) ` z ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` z ) )
3 fveq2 
 |-  ( z = B -> ( rec ( ( x e. _V |-> suc x ) , A ) ` z ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )
4 df-oadd 
 |-  +o = ( y e. On , z e. On |-> ( rec ( ( x e. _V |-> suc x ) , y ) ` z ) )
5 fvex 
 |-  ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) e. _V
6 2 3 4 5 ovmpo 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )