Successor is Less than Successor/Sufficient Condition/Proof 1

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

Suppose $y^+ \in x^+$.

By the definition of successor, $y^+ \in x \lor y^+ = x$.

Suppose $y^+ = x$.

By Ordinal is Less than Successor, $y \in x$.

Suppose $y^+ \in x$.

By Ordinal is Less than Successor, $y \in y^+$.

By Ordinal is Transitive, $y \in x$.

$\blacksquare$