# Ordinal is Subset of Successor

## Theorem

Let $x$ and $y$ be ordinals.

Let $x^+$ denote the successor of $x$.

Then:

$x \subseteq y^+ \iff \left({x \subseteq y \lor x = y^+}\right)$

## Proof

Let $A \subset B$ denote that $A$ is a proper subset of $B$.

Let $A \in B$ denote that $A$ is an element of $B$.

From Transitive Set is Proper Subset of Ordinal iff Element of Ordinal, $\subset$ and $\in$ can be used interchangeably.

Thus:

 $\ds x \subseteq y$ $\leadsto$ $\ds x \subseteq y^+$ Ordinal is Less than Successor $\ds x = y^+$ $\leadsto$ $\ds x \subseteq y^+$ Definition 2 of Set Equality
 $\ds x \subseteq y^+$ $\leadsto$ $\ds \paren {x \subset y^+ \lor x = y^+}$ $\ds x \subset y^+$ $\leadsto$ $\ds x \in y^+$ Transitive Set is Proper Subset of Ordinal iff Element of Ordinal $\ds$ $\leadsto$ $\ds \paren {x = y \lor x \in y}$ Definition of Successor Set $\ds$ $\leadsto$ $\ds x \subseteq y$ Transitive Set is Proper Subset of Ordinal iff Element of Ordinal

$\blacksquare$