# Successor of Ordinal Smaller than Limit Ordinal is also Smaller

Jump to navigation
Jump to search

## Theorem

Let $\On$ denote the class of all ordinals.

Let $\lambda \in \On$ be a limit ordinal.

Then:

- $\forall \alpha \in \On: \alpha < \lambda \implies \alpha^+ < \lambda$

## Proof 1

Let $\lambda$ be a limit ordinal such that $\alpha < \lambda$.

From Successor of Element of Ordinal is Subset

Then as $\alpha^+$ is the successor set of $\alpha$ it follows that:

- $\alpha^+ \le \lambda$

This article, or a section of it, needs explaining.Find the result that says $\alpha < \beta \implies \alpha^+ \le \beta$You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Explain}}` from the code. |

But as $\lambda$ is not a successor ordinal:

- $\alpha^+ \ne \lambda$

Hence:

- $\alpha^+ < \lambda$

$\blacksquare$

## Proof 2

Because $\lambda$ is a limit ordinal:

- $\lambda \ne \alpha^+$

Moreover, by Successor of Element of Ordinal is Subset:

- $\alpha \in \lambda \implies \alpha^+ \subseteq \lambda$

Therefore by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal:

- $\alpha^+ \subset \lambda$ and $\alpha^+ \in \lambda$

$\blacksquare$

This page has been identified as a candidate for refactoring.Yes I appreciate that these two proofs are just about the same, but until we have rigorously reviewed the flow of implications from the two complementary axiom systems that define what an ordinal is, we can't afford to be slackUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |