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 \in On \land Lim B \land B \in V) \to Lim (A +_{𝑜} B)$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in On \land Lim B \land B \in V) \to A \in On$
2		simp3	$⊢ (A \in On \land Lim B \land B \in V) \to B \in V$
3		simp2	$⊢ (A \in On \land Lim B \land B \in V) \to Lim B$
4		oalimcl	$⊢ (A \in On \land (B \in V \land Lim B)) \to Lim (A +_{𝑜} B)$
5	1 2 3 4	syl12anc	$⊢ (A \in On \land Lim B \land B \in V) \to Lim (A +_{𝑜} B)$