Description: Given a limit ordinal, the power of any base at least as large as two raised to an ordinal less than that limit ordinal is less than the power of that base raised to the limit ordinal . Lemma 3.22 of Schloeder p. 10. See oeordi . (Contributed by RP, 30-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | oeord2lim | |- ( ( ( A e. On /\ 1o e. A ) /\ ( Lim C /\ C e. V ) ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | limelon | |- ( ( C e. V /\ Lim C ) -> C e. On ) |
|
| 2 | 1 | ancoms | |- ( ( Lim C /\ C e. V ) -> C e. On ) |
| 3 | ondif2 | |- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) ) |
|
| 4 | 3 | biimpri | |- ( ( A e. On /\ 1o e. A ) -> A e. ( On \ 2o ) ) |
| 5 | oeordi | |- ( ( C e. On /\ A e. ( On \ 2o ) ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |
|
| 6 | 2 4 5 | syl2anr | |- ( ( ( A e. On /\ 1o e. A ) /\ ( Lim C /\ C e. V ) ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |