Metamath Proof Explorer

Theorem om0

Description: Ordinal multiplication with zero. Definition 8.15(a) of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. See om0x for a way to remove the antecedent A e. On . (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		omv	$⊢ (A \in On \land \emptyset \in On) \to A \cdot_{𝑜} \emptyset = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (\emptyset)$
3	1 2	mpan2	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (\emptyset)$
4		0ex	$⊢ \emptyset \in V$
5	4	rdg0	$⊢ rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (\emptyset) = \emptyset$
6	3 5	eqtrdi	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$