oe0m

Description: Value of zero raised to an ordinal. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oe0m	$⊢ A \in On \to \emptyset ↑_{𝑜} A = 1_{𝑜} ∖ A$

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		oev	$⊢ (\emptyset \in On \land A \in On) \to \emptyset ↑_{𝑜} A = if (\emptyset = \emptyset, 1_{𝑜} ∖ A, rec ((x \in V ⟼ x \cdot_{𝑜} \emptyset), 1_{𝑜}) (A))$
3	1 2	mpan	$⊢ A \in On \to \emptyset ↑_{𝑜} A = if (\emptyset = \emptyset, 1_{𝑜} ∖ A, rec ((x \in V ⟼ x \cdot_{𝑜} \emptyset), 1_{𝑜}) (A))$
4		eqid	$⊢ \emptyset = \emptyset$
5	4	iftruei	$⊢ if (\emptyset = \emptyset, 1_{𝑜} ∖ A, rec ((x \in V ⟼ x \cdot_{𝑜} \emptyset), 1_{𝑜}) (A)) = 1_{𝑜} ∖ A$
6	3 5	eqtrdi	$⊢ A \in On \to \emptyset ↑_{𝑜} A = 1_{𝑜} ∖ A$

Metamath Proof Explorer