oevn0

Description: Value of ordinal exponentiation at a nonzero base. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

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

Step	Hyp	Ref	Expression
1		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
2		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
3	1 2	bitrdi	$⊢ A \in On \to (\emptyset \in A \leftrightarrow \neg A = \emptyset)$
4	3	adantr	$⊢ (A \in On \land B \in On) \to (\emptyset \in A \leftrightarrow \neg A = \emptyset)$
5		oev	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B = if (A = \emptyset, 1_{𝑜} ∖ B, rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B))$
6		iffalse	$⊢ \neg A = \emptyset \to if (A = \emptyset, 1_{𝑜} ∖ B, rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)) = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)$
7	5 6	sylan9eq	$⊢ ((A \in On \land B \in On) \land \neg A = \emptyset) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)$
8	7	ex	$⊢ (A \in On \land B \in On) \to (\neg A = \emptyset \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B))$
9	4 8	sylbid	$⊢ (A \in On \land B \in On) \to (\emptyset \in A \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B))$
10	9	imp	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)$

Metamath Proof Explorer