Successor of Element of Ordinal is Subset

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ and $y$ be ordinals.


Then:

$x \in y \iff x^+ \subseteq y$


Proof

\(\ds x\) \(\in\) \(\ds y\)
\(\ds \leadstoandfrom \ \ \) \(\ds x^+\) \(\in\) \(\ds y^+\) Successor is Less than Successor
\(\ds \leadstoandfrom \ \ \) \(\ds x^+\) \(\in\) \(\ds y\) Definition of Successor Set
\(\, \ds \lor \, \) \(\ds x^+\) \(=\) \(\ds y\)
\(\ds \leadstoandfrom \ \ \) \(\ds x^+\) \(\subsetneq\) \(\ds y\) Transitive Set is Proper Subset of Ordinal iff Element of Ordinal
\(\, \ds \lor \, \) \(\ds x^+\) \(=\) \(\ds y\)
\(\ds \leadstoandfrom \ \ \) \(\ds x^+\) \(\subseteq\) \(\ds y\)

$\blacksquare$