Successor of Ordinal Smaller than Limit Ordinal is also Smaller

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. In particular: 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 needs the help of a knowledgeable authority. In particular: 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 slack If you are knowledgeable in this area, then you can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues. 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 {{Help}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.