# Subset is Right Compatible with Ordinal Addition

## 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$