omv

Description: Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	omv	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B)$

Step	Hyp	Ref	Expression
1		oveq2	$⊢ y = A \to x +_{𝑜} y = x +_{𝑜} A$
2	1	mpteq2dv	$⊢ y = A \to (x \in V ⟼ x +_{𝑜} y) = (x \in V ⟼ x +_{𝑜} A)$
3		rdgeq1	$⊢ (x \in V ⟼ x +_{𝑜} y) = (x \in V ⟼ x +_{𝑜} A) \to rec ((x \in V ⟼ x +_{𝑜} y), \emptyset) = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset)$
4	2 3	syl	$⊢ y = A \to rec ((x \in V ⟼ x +_{𝑜} y), \emptyset) = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset)$
5	4	fveq1d	$⊢ y = A \to rec ((x \in V ⟼ x +_{𝑜} y), \emptyset) (z) = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (z)$
6		fveq2	$⊢ z = B \to rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (z) = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B)$
7		df-omul	$⊢ \cdot_{𝑜} = (y \in On, z \in On ⟼ rec ((x \in V ⟼ x +_{𝑜} y), \emptyset) (z))$
8		fvex	$⊢ rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B) \in V$
9	5 6 7 8	ovmpo	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B)$

Metamath Proof Explorer