df-omul

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

		Ref	Expression
	Assertion	df-omul	$⊢ \cdot_{𝑜} = (x \in On, y \in On ⟼ rec ((z \in V ⟼ z +_{𝑜} x), \emptyset) (y))$

Step	Hyp	Ref	Expression
0		comu	$class \cdot_{𝑜}$
1		vx	$setvar x$
2		con0	$class On$
3		vy	$setvar y$
4		vz	$setvar z$
5		cvv	$class V$
6	4	cv	$setvar z$
7		coa	$class +_{𝑜}$
8	1	cv	$setvar x$
9	6 8 7	co	$class (z +_{𝑜} x)$
10	4 5 9	cmpt	$class (z \in V ⟼ z +_{𝑜} x)$
11		c0	$class \emptyset$
12	10 11	crdg	$class rec ((z \in V ⟼ z +_{𝑜} x), \emptyset)$
13	3	cv	$setvar y$
14	13 12	cfv	$class rec ((z \in V ⟼ z +_{𝑜} x), \emptyset) (y)$
15	1 3 2 2 14	cmpo	$class (x \in On, y \in On ⟼ rec ((z \in V ⟼ z +_{𝑜} x), \emptyset) (y))$
16	0 15	wceq	$wff \cdot_{𝑜} = (x \in On, y \in On ⟼ rec ((z \in V ⟼ z +_{𝑜} x), \emptyset) (y))$

Metamath Proof Explorer