Subset is Compatible with Ordinal Successor
Theorem
Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.
Let $x \in y$.
Then:
- $x^+ \in y^+$
Proof 1
\(\ds x \in y\) | \(\implies\) | \(\ds x \ne y\) | No Membership Loops | |||||||||||
\(\ds \) | \(\implies\) | \(\ds x^+ \ne y^+\) | Equality of Successors | |||||||||||
\(\ds x \in y\) | \(\implies\) | \(\ds y \notin x\) | No Membership Loops | |||||||||||
\(\ds \) | \(\implies\) | \(\ds y \notin x^+\) | $x ≠ y$ and Definition of Successor Set | |||||||||||
\(\ds y^+ \in x^+\) | \(\implies\) | \(\ds y \in x^+\) | Successor Set of Ordinal is Ordinal, Ordinals are Transitive, and Set is Element of Successor |
The last part is a contradiction, so $y^+ \notin x^+$.
By Ordinal Membership is Trichotomy:
- $x^+ \in y^+$
$\blacksquare$
Proof 2
First note that by Successor Set of Ordinal is Ordinal, $x^+$ and $y^+$ are ordinals.
Let $x \in y$.
We wish to show that $x^+ \in y^+$.
By Ordinal Membership is Trichotomy:
- Either $x^+ \in y^+$, $y^+ \in x^+$, or $x^+ = y^+$.
Aiming for a contradiction, suppose $y^+ = x^+$.
Then $y \in x$ or $y = x$ by the definition of successor set.
If $y = x$ then $x \in x$, contradicting the fact that Ordinal is not Element of Itself.
If $y \in x$ then since an ordinal is transitive, $y \in y$, again contradicting Ordinal is not Element of Itself.
Thus $y^+ ≠ x^+$.
Aiming for a contradiction, suppose $y^+ \in x^+$.
By definition of successor set, $y^+ \in x$ or $y^+ = x$.
If $y^+ \in x$, then since $y^+$ and $x$ are both ordinals, $y^+ \subsetneqq x$.
Then $y \in x$.
Since $y$ is transitive, $y \in y$, contradicting Ordinal is not Element of Itself.
If instead $y^+ = x$, then $x \in y \in y^+ = x$, so the same contradiction arises because $x$ is transitive.
Thus $y^+ \notin x^+$.
So the only remaining possibility, that $x^+ \in y^+$, must hold.
$\blacksquare$
Proof 3
First note that by Successor Set of Ordinal is Ordinal, $x^+$ and $y^+$ are ordinals.
By Ordinal Membership is Trichotomy, one of the following must be true:
\(\ds x^+\) | \(=\) | \(\ds y^+\) | ||||||||||||
\(\ds y^+\) | \(\in\) | \(\ds x^+\) | ||||||||||||
\(\ds x^+\) | \(\in\) | \(\ds y^+\) |
We will show that the first two are both false, so that the third must hold.
Two preliminary facts:
\((1)\) | $:$ | \(\ds x \) | \(\ds \ne \) | \(\ds y \) | $x \in y$ and Ordinal is not Element of Itself | ||||
\((2)\) | $:$ | \(\ds y \) | \(\ds \notin \) | \(\ds x \) | $x \in y$ and Ordinal Membership is Asymmetric |
By $(1)$ and Equality of Successors:
- $x^+ \ne y^+$
Thus the first of the three possibilities is false.
Aiming for a contradiction, suppose $y^+ \in x^+$.
Then:
\(\ds y\) | \(\in\) | \(\ds y^+\) | Definition of Successor Set | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds y\) | \(\in\) | \(\ds x^+\) | $y^+ \in x^+$ and $x^+$ is an ordinal and therefore transitive. | ||||||||||
\(\ds \leadsto \ \ \) | \(\ds y\) | \(\in\) | \(\ds x\) | Definition of Successor Set | ||||||||||
\(\, \ds \lor \, \) | \(\ds y\) | \(=\) | \(\ds x\) |
But we already know that $y \notin x$ by $(2)$ and $y \ne x$ by $(1)$.
So this is a contradiction, and we conclude that $y^+ \notin x^+$.
Thus we have shown that the second possibility is false.
Thus the third and final one must hold: $x^+ \in y^+$.
$\blacksquare$