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 e. On /\ 1o e. A ) /\ ( Lim B /\ B e. V ) ) -> Lim ( A ^o B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ondif2 | |- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) ) |
|
| 2 | 1 | biimpri | |- ( ( A e. On /\ 1o e. A ) -> A e. ( On \ 2o ) ) |
| 3 | pm3.22 | |- ( ( Lim B /\ B e. V ) -> ( B e. V /\ Lim B ) ) |
|
| 4 | oelimcl | |- ( ( A e. ( On \ 2o ) /\ ( B e. V /\ Lim B ) ) -> Lim ( A ^o B ) ) |
|
| 5 | 2 3 4 | syl2an | |- ( ( ( A e. On /\ 1o e. A ) /\ ( Lim B /\ B e. V ) ) -> Lim ( A ^o B ) ) |