Definition df-oadd

Description: Define the ordinal addition operation. (Contributed by NM, 3-May-1995)

	Ref	Expression
Assertion	df-oadd	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coa	|- +o
1		vx	|- x
2		con0	|- On
3		vy	|- y
4		vz	|- z
5		cvv	|- _V
6	4	cv	|- z
7	6	csuc	|- suc z
8	4 5 7	cmpt	|- ( z e. _V |-> suc z )
9	1	cv	|- x
10	8 9	crdg	|- rec ( ( z e. _V |-> suc z ) , x )
11	3	cv	|- y
12	11 10	cfv	|- ( rec ( ( z e. _V |-> suc z ) , x ) ` y )
13	1 3 2 2 12	cmpo	|- ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
14	0 13	wceq	|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )