# Subset is Right Compatible with Ordinal Exponentiation

## Theorem

Let $x, y, z$ be ordinals.

Then:

$x \le y \implies x^z \le y^z$

## Proof

The proof shall proceed by Transfinite Induction on $z$.

### Basis for the Induction

If $z = \varnothing$, then $x^z = 1$

 $\displaystyle x^z$ $=$ $\displaystyle 1$ Definition of Ordinal Exponentiation $\displaystyle y^z$ $=$ $\displaystyle 1$ Definition of Ordinal Exponentiation $\displaystyle x^z$ $\le$ $\displaystyle y^z$ Set is Subset of Itself

This proves the basis for the induction.

$\Box$

### Induction Step

The inductive hypothesis states that $x^z \le y^z$ for $y$.

Then:

 $\displaystyle x^{z^+}$ $=$ $\displaystyle x^z \times x$ Definition of Ordinal Exponentiation $\displaystyle$ $\le$ $\displaystyle x^z \times y$ Membership is Left Compatible with Ordinal Multiplication $\displaystyle$ $\le$ $\displaystyle y^z \times y$ Subset is Right Compatible with Ordinal Multiplication $\displaystyle$ $=$ $\displaystyle y^{z^+}$ Definition of Ordinal Exponentiation

This proves the induction step.

$\Box$

### Limit Case

The inductive hypothesis for the limit case states that:

$\forall w \in z: x^w \le y^w$ where $z$ is a limit ordinal.

 $\, \displaystyle \forall w \in z: \,$ $\displaystyle x^w$ $\subseteq$ $\displaystyle y^w$ Inductive Hypothesis $\displaystyle \implies \ \$ $\displaystyle \bigcup_{w \mathop \in z} x^w$ $\subseteq$ $\displaystyle \bigcup_{w \mathop \in z} y^w$ by Indexed Union Subset $\displaystyle \implies \ \$ $\displaystyle x^z$ $\subseteq$ $\displaystyle y^z$ Definition of Ordinal Exponentiation

This proves the limit case.

$\blacksquare$