oe0suclim

Description: Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of Schloeder p. 4. See oe0 , oesuc , oe0m1 , and oelim . (Contributed by RP, 18-Jan-2025)

		Ref	Expression
	Assertion	oe0suclim	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \to A ↑_{𝑜} B = 1_{𝑜}) \land ((B = suc C \land C \in On) \to A ↑_{𝑜} B = (A ↑_{𝑜} C) \cdot_{𝑜} A) \land (Lim B \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)))$

Proof

Step	Hyp	Ref	Expression
1		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
2		oesuc	$⊢ (A \in On \land C \in On) \to A ↑_{𝑜} suc C = (A ↑_{𝑜} C) \cdot_{𝑜} A$
3		oelim	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = ⋃_{c \in B} (A ↑_{𝑜} c)$
4		simpr	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to \emptyset \in A$
5	4	iftrued	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset) = ⋃_{c \in B} (A ↑_{𝑜} c)$
6	3 5	eqtr4d	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)$
7		simpl	$⊢ (A \in On \land (B \in On \land Lim B)) \to A \in On$
8		0elon	$⊢ \emptyset \in On$
9		ontri1	$⊢ (A \in On \land \emptyset \in On) \to (A \subseteq \emptyset \leftrightarrow \neg \emptyset \in A)$
10		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
11	9 10	biimtrrdi	$⊢ (A \in On \land \emptyset \in On) \to (\neg \emptyset \in A \to A = \emptyset)$
12	7 8 11	sylancl	$⊢ (A \in On \land (B \in On \land Lim B)) \to (\neg \emptyset \in A \to A = \emptyset)$
13		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
14		oe0m1	$⊢ B \in On \to (\emptyset \in B \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
15	14	biimpd	$⊢ B \in On \to (\emptyset \in B \to \emptyset ↑_{𝑜} B = \emptyset)$
16		0ellim	$⊢ Lim B \to \emptyset \in B$
17	15 16	impel	$⊢ (B \in On \land Lim B) \to \emptyset ↑_{𝑜} B = \emptyset$
18	17	adantl	$⊢ (A \in On \land (B \in On \land Lim B)) \to \emptyset ↑_{𝑜} B = \emptyset$
19	13 18	sylan9eqr	$⊢ ((A \in On \land (B \in On \land Lim B)) \land A = \emptyset) \to A ↑_{𝑜} B = \emptyset$
20	19	ex	$⊢ (A \in On \land (B \in On \land Lim B)) \to (A = \emptyset \to A ↑_{𝑜} B = \emptyset)$
21	12 20	syld	$⊢ (A \in On \land (B \in On \land Lim B)) \to (\neg \emptyset \in A \to A ↑_{𝑜} B = \emptyset)$
22	21	imp	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \neg \emptyset \in A) \to A ↑_{𝑜} B = \emptyset$
23		simpr	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \neg \emptyset \in A) \to \neg \emptyset \in A$
24	23	iffalsed	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \neg \emptyset \in A) \to if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset) = \emptyset$
25	22 24	eqtr4d	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \neg \emptyset \in A) \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)$
26	6 25	pm2.61dan	$⊢ (A \in On \land (B \in On \land Lim B)) \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)$
27	26	anassrs	$⊢ ((A \in On \land B \in On) \land Lim B) \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)$
28	1 2 27	onov0suclim	$⊢ (A \in On \land B \in On) \to ((B = \emptyset \to A ↑_{𝑜} B = 1_{𝑜}) \land ((B = suc C \land C \in On) \to A ↑_{𝑜} B = (A ↑_{𝑜} C) \cdot_{𝑜} A) \land (Lim B \to A ↑_{𝑜} B = if (\emptyset \in A, ⋃_{c \in B} (A ↑_{𝑜} c), \emptyset)))$

Metamath Proof Explorer

Theorem oe0suclim

Proof