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	|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A +o B ) = A ) /\ ( ( B = suc C /\ C e. On ) -> ( A +o B ) = suc ( A +o C ) ) /\ ( Lim B -> ( A +o B ) = U_ c e. B ( A +o c ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oa0	|- ( A e. On -> ( A +o (/) ) = A )
2		oasuc	|- ( ( A e. On /\ C e. On ) -> ( A +o suc C ) = suc ( A +o C ) )
3		oalim	|- ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( A +o B ) = U_ c e. B ( A +o c ) )
4	3	anassrs	|- ( ( ( A e. On /\ B e. On ) /\ Lim B ) -> ( A +o B ) = U_ c e. B ( A +o c ) )
5	1 2 4	onov0suclim	|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A +o B ) = A ) /\ ( ( B = suc C /\ C e. On ) -> ( A +o B ) = suc ( A +o C ) ) /\ ( Lim B -> ( A +o B ) = U_ c e. B ( A +o c ) ) ) )