Description: Ordinal exponentiation of the same base at least as large as two preserves the ordering of the exponents. Lemma 3.23 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | oeord2i | |- ( ( ( A e. On /\ 1o e. A ) /\ C e. On ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |
| 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 | 2 | anim1ci | |- ( ( ( A e. On /\ 1o e. A ) /\ C e. On ) -> ( C e. On /\ A e. ( On \ 2o ) ) ) |
| 4 | oeordi | |- ( ( C e. On /\ A e. ( On \ 2o ) ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |
|
| 5 | 3 4 | syl | |- ( ( ( A e. On /\ 1o e. A ) /\ C e. On ) -> ( B e. C -> ( A ^o B ) e. ( A ^o C ) ) ) |