Description: Ordinal one plus omega is equal to omega. See oaabs for the sum of any natural number on the left and ordinal at least as large as omega on the right. Lemma 3.8 of Schloeder p. 8. See oaabs2 where a power of omega is the upper bound of the left and a lower bound on the right. (Contributed by RP, 29-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 1oaomeqom | |- ( 1o +o _om ) = _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omelon | |- _om e. On |
|
| 2 | 1onn | |- 1o e. _om |
|
| 3 | oaabslem | |- ( ( _om e. On /\ 1o e. _om ) -> ( 1o +o _om ) = _om ) |
|
| 4 | 1 2 3 | mp2an | |- ( 1o +o _om ) = _om |