This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oe0m0

Description: Ordinal exponentiation with zero base and zero exponent. Proposition 8.31 of TakeutiZaring p. 67. (Contributed by NM, 31-Dec-2004)

		Ref	Expression
	Assertion	oe0m0	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜}$

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		oe0m	$⊢ \emptyset \in On \to \emptyset ↑_{𝑜} \emptyset = 1_{𝑜} ∖ \emptyset$
3	1 2	ax-mp	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜} ∖ \emptyset$
4		dif0	$⊢ 1_{𝑜} ∖ \emptyset = 1_{𝑜}$
5	3 4	eqtri	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜}$