Ordinal is not Element of Itself

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ be an ordinal.


Then $x \notin x$.


Proof 1

By Successor Set of Ordinal is Ordinal, the successor of $x$ is an ordinal.

That is, $x^+ = x \cup \set x$ is an ordinal.

By Set is Element of Successor, $x \in x^+$.

Because $x^+$ is an ordinal, it is strictly well-ordered by the epsilon restriction $\Epsilon {\restriction_{x^+} }$.


Because a strict ordering is antireflexive and $x \in x^+$, we conclude that $x \notin x$.

$\blacksquare$


Proof 2

This result follows immediately from Set is Not Element of Itself.

$\blacksquare$