Metamath Proof Explorer

Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. Definition 2.6 of Schloeder p. 4. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} \emptyset = \emptyset ↑_{𝑜} \emptyset$
2		oe0m0	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜}$
3	1 2	eqtrdi	$⊢ A = \emptyset \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
4	3	adantl	$⊢ (A \in On \land A = \emptyset) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
5		0elon	$⊢ \emptyset \in On$
6		oevn0	$⊢ ((A \in On \land \emptyset \in On) \land \emptyset \in A) \to A ↑_{𝑜} \emptyset = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (\emptyset)$
7	5 6	mpanl2	$⊢ (A \in On \land \emptyset \in A) \to A ↑_{𝑜} \emptyset = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (\emptyset)$
8		1oex	$⊢ 1_{𝑜} \in V$
9	8	rdg0	$⊢ rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (\emptyset) = 1_{𝑜}$
10	7 9	eqtrdi	$⊢ (A \in On \land \emptyset \in A) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
11	10	adantll	$⊢ ((A \in On \land A \in On) \land \emptyset \in A) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
12	4 11	oe0lem	$⊢ (A \in On \land A \in On) \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
13	12	anidms	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$