Definition df-omul 3107

Description: Define the ordinal multiplication operation.

Assertion

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

Distinct variable group(s):   x,y,z,w,v

Detailed syntax breakdown of Definition df-omul

Step	Hyp	Ref	Expression
1		comu 3102	. 2 class .o
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		con0 2199	. . . . . 6 class On
5	3, 4	wcel 1092	. . . . 5 wff x e. On
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. On
9	5, 8	wa 196	. . . 4 wff (x e. On /\ y e. On)
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12		vv	. . . . . . . . . 10 set v
13	12	cv 1089	. . . . . . . . 9 class v
14		vw	. . . . . . . . . . 11 set w
15	14	cv 1089	. . . . . . . . . 10 class w
16		coa 3101	. . . . . . . . . 10 class +o
17	15, 3, 16	co 3001	. . . . . . . . 9 class (w +o x)
18	13, 17	wceq 1091	. . . . . . . 8 wff v = (w +o x)
19	18, 14, 12	copab 2055	. . . . . . 7 class {<.w, v>. | v = (w +o x)}
20		c0 1707	. . . . . . 7 class (/)
21	19, 20	crdg 2969	. . . . . 6 class rec({<.w, v>. | v = (w +o x)}, (/))
22	7, 21	cfv 2422	. . . . 5 class (rec({<.w, v>. | v = (w +o x)}, (/))` y)
23	11, 22	wceq 1091	. . . 4 wff z = (rec({<.w, v>. | v = (w +o x)}, (/))` y)
24	9, 23	wa 196	. . 3 wff ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = (w +o x)}, (/))` y))
25	24, 2, 6, 10	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = (w +o x)}, (/))` y))}
26	1, 25	wceq 1091	1 wff .o = {<.<.x, y>., z>. | ((x e. On /\ y e. On) /\ z = (rec({<.w, v>. | v = (w +o x)}, (/))` y))}

This definition is referenced by:  fnom 3118  omv 3120

metamath.org