Metamath Proof Explorer

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 
|- ( ( A e. On /\ Lim B /\ B e. V ) -> Lim ( A +o B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. On /\ Lim B /\ B e. V ) -> A e. On )
2 simp3 
 |-  ( ( A e. On /\ Lim B /\ B e. V ) -> B e. V )
3 simp2 
 |-  ( ( A e. On /\ Lim B /\ B e. V ) -> Lim B )
4 oalimcl 
 |-  ( ( A e. On /\ ( B e. V /\ Lim B ) ) -> Lim ( A +o B ) )
5 1 2 3 4 syl12anc 
 |-  ( ( A e. On /\ Lim B /\ B e. V ) -> Lim ( A +o B ) )