No Ordinal Between Set and Successor

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ be an ordinal.


Then, no ordinal $y$ exists between $x$ and its successor:

$\neg \exists y: \left({x \prec y \prec x^+}\right)$


Proof

We will proceed by contradiction.

Assume such an ordinal $y$ exists.


Then, by Ordering on Ordinal is Subset Relation:

$x \in y$

and from Transitive Set is Proper Subset of Ordinal iff Element of Ordinal:

$y \in x^+$


Applying the definition of a successor set, we have:

$y \in x \lor y = x$

But this creates a membership loop, in that:

$x \in y \in x \lor x \in x$


By No Membership Loops, we have created a contradiction.

The result follows from Proof by Contradiction.

$\blacksquare$


Sources