Subset is Right Compatible with Ordinal Addition

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x, y, z$ be ordinals.


Then:

$x \le y \implies \paren {x + z} \le \paren {y + z}$


Proof

The proof proceeds by transfinite induction on $z$.


Base Case

\(\ds x + \O\) \(=\) \(\ds x\) Definition of Ordinal Addition
\(\ds y + \O\) \(=\) \(\ds y\) Definition of Ordinal Addition
\(\ds \leadsto \ \ \) \(\ds x \le y\) \(\implies\) \(\ds \paren {x + \O} \le \paren {y + \O}\) Substitutivity of Equality


Inductive Case

\(\ds x\) \(\le\) \(\ds y\)
\(\ds \leadsto \ \ \) \(\ds \paren {x + z}\) \(\le\) \(\ds \paren {y + z}\) Induction Hypothesis
\(\ds \leadsto \ \ \) \(\ds \paren {x + z}^+\) \(\le\) \(\ds \paren {y + z}^+\) Successor Preserved under Subset
\(\ds \leadsto \ \ \) \(\ds \paren {x + z^+}\) \(\le\) \(\ds \paren {y + z^+}\) Definition of Ordinal Addition


Limit Case

\(\ds \forall w < z: \, \) \(\ds x \le y\) \(\implies\) \(\ds \paren {x + w} \le \paren {y + w}\)
\(\ds \leadsto \ \ \) \(\ds x \le y\) \(\implies\) \(\ds \forall w < z: \paren {x + w} \le \paren {y + w}\)
\(\ds \leadsto \ \ \) \(\ds x \le y\) \(\implies\) \(\ds \bigcup_{w \mathop \in z} \paren {x + w} \le \bigcup_{w \mathop \in z} \paren {y + w}\) Indexed Union Subset
\(\ds \leadsto \ \ \) \(\ds x \le y\) \(\implies\) \(\ds \paren {x + z} \le \paren {y + z}\) Definition of Ordinal Addition

The result follows by transfinite induction.

$\blacksquare$


Sources