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	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → Lim ( 𝐴 ↑o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ondif2	⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
2	1	biimpri	⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) → 𝐴 ∈ ( On ∖ 2o ) )
3		pm3.22	⊢ ( ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ Lim 𝐵 ) )
4		oelimcl	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ ( 𝐵 ∈ 𝑉 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 ↑o 𝐵 ) )
5	2 3 4	syl2an	⊢ ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → Lim ( 𝐴 ↑o 𝐵 ) )