Metamath Proof Explorer

Theorem rp-oelim2

Description: The power of an ordinal at least as large as two with a limit ordinal on thr right is a limit ordinal. Lemma 3.21 of Schloeder p. 10. See oelimcl . (Contributed by RP, 30-Jan-2025)

		Ref	Expression
	Assertion	rp-oelim2	$⊢ ((A \in On \land 1_{𝑜} \in A) \land (Lim B \land B \in V)) \to Lim (A ↑_{𝑜} B)$

Proof

Step	Hyp	Ref	Expression
1		ondif2	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$
2	1	biimpri	$⊢ (A \in On \land 1_{𝑜} \in A) \to A \in (On ∖ 2_{𝑜})$
3		pm3.22	$⊢ (Lim B \land B \in V) \to (B \in V \land Lim B)$
4		oelimcl	$⊢ (A \in (On ∖ 2_{𝑜}) \land (B \in V \land Lim B)) \to Lim (A ↑_{𝑜} B)$
5	2 3 4	syl2an	$⊢ ((A \in On \land 1_{𝑜} \in A) \land (Lim B \land B \in V)) \to Lim (A ↑_{𝑜} B)$