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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 +o 𝐵 ) = 𝐴 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 +o 𝐵 ) = suc ( 𝐴 +o 𝐶 ) ) ∧ ( Lim 𝐵 → ( 𝐴 +o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 +o 𝑐 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
2		oasuc	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +o suc 𝐶 ) = suc ( 𝐴 +o 𝐶 ) )
3		oalim	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( 𝐴 +o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 +o 𝑐 ) )
4	3	anassrs	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐴 +o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 +o 𝑐 ) )
5	1 2 4	onov0suclim	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 +o 𝐵 ) = 𝐴 ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 +o 𝐵 ) = suc ( 𝐴 +o 𝐶 ) ) ∧ ( Lim 𝐵 → ( 𝐴 +o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 +o 𝑐 ) ) ) )