Theorem oa0suclim

Description: Closed form expression of the value of ordinal addition for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.3 of Schloeder p. 4. See oa0 , oasuc , and oalim . (Contributed by RP, 18-Jan-2025)

	Ref	Expression
Assertion	oa0suclim	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(B=\varnothing \to A{+}_{𝑜}B=A\right)\wedge \left(\left(B=\mathrm{suc}C\wedge C\in \mathrm{On}\right)\to A{+}_{𝑜}B=\mathrm{suc}\left(A{+}_{𝑜}C\right)\right)\wedge \left(\mathrm{Lim}B\to A{+}_{𝑜}B=\bigcup _{c\in B}\left(A{+}_{𝑜}c\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
2		oasuc	$$⊢\left(A\in \mathrm{On}\wedge C\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}C=\mathrm{suc}\left(A{+}_{𝑜}C\right)$$
3		oalim	$$⊢\left(A\in \mathrm{On}\wedge \left(B\in \mathrm{On}\wedge \mathrm{Lim}B\right)\right)\to A{+}_{𝑜}B=\bigcup _{c\in B}\left(A{+}_{𝑜}c\right)$$
4	3	anassrs	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \mathrm{Lim}B\right)\to A{+}_{𝑜}B=\bigcup _{c\in B}\left(A{+}_{𝑜}c\right)$$
5	1 2 4	onov0suclim	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\left(B=\varnothing \to A{+}_{𝑜}B=A\right)\wedge \left(\left(B=\mathrm{suc}C\wedge C\in \mathrm{On}\right)\to A{+}_{𝑜}B=\mathrm{suc}\left(A{+}_{𝑜}C\right)\right)\wedge \left(\mathrm{Lim}B\to A{+}_{𝑜}B=\bigcup _{c\in B}\left(A{+}_{𝑜}c\right)\right)\right)$$