Theorem oalim2cl

Description: The ordinal sum of any ordinal with a limit ordinal on the right is a limit ordinal. (Contributed by RP, 6-Feb-2025)

	Ref	Expression
Assertion	oalim2cl	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → Lim ( 𝐴 +o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ On )
2		simp3	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
3		simp2	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → Lim 𝐵 )
4		oalimcl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝑉 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 +o 𝐵 ) )
5	1 2 3 4	syl12anc	⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → Lim ( 𝐴 +o 𝐵 ) )