Ordinal is not Element of Itself/Proof 1
Jump to navigation
Jump to search
Theorem
Let $x$ be an ordinal.
Then:
- $x \notin x$
Proof
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$