Definition df-omul

Description: Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995)

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

Detailed syntax breakdown

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