Definition df-oadd 5179

Description: Define the ordinal addition operation.

Assertion

Ref	Expression
df-oadd	|- +o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = suc w}, x)` y))}

Distinct variable group:   x,y,z,w,v

Detailed syntax breakdown of Definition df-oadd

Step	Hyp	Ref	Expression
1		coa 5174	. 2 class +o
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		con0 3657	. . . . . 6 class On
5	3, 4	wcel 1300	. . . . 5 wff x e. On
6		vy	. . . . . . 7 set y
7	6	cv 1297	. . . . . 6 class y
8	7, 4	wcel 1300	. . . . 5 wff y e. On
9	5, 8	wa 240	. . . 4 wff (x e. On /\ y e. On)
10		vz	. . . . . 6 set z
11	10	cv 1297	. . . . 5 class z
12		vv	. . . . . . . . . 10 set v
13	12	cv 1297	. . . . . . . . 9 class v
14		vw	. . . . . . . . . . 11 set w
15	14	cv 1297	. . . . . . . . . 10 class w
16	15	csuc 3659	. . . . . . . . 9 class suc w
17	13, 16	wceq 1298	. . . . . . . 8 wff v = suc w
18	17, 14, 12	copab 3395	. . . . . . 7 class {<.w, v>. | v = suc w}
19	18, 3	crdg 5139	. . . . . 6 class rec({<.w, v>. | v = suc w}, x)
20	7, 19	cfv 3998	. . . . 5 class (rec({<.w, v>. | v = suc w}, x)` y)
21	11, 20	wceq 1298	. . . 4 wff z = (rec({<.w, v>. | v = suc w}, x)` y)
22	9, 21	wa 240	. . 3 wff ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = suc w}, x)` y))
23	22, 2, 6, 10	copab2 4885	. 2 class {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = suc w}, x)` y))}
24	1, 23	wceq 1298	1 wff +o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = suc w}, x)` y))}

This definition is referenced by:  fnoa 5193  oav 5195

Copyright terms: Public domain