# Ordinal Power of Power

## Theorem

Let $x$, $y$, and $z$ be ordinals.

Then:

$\left({x^y}\right)^z = x^{y \mathop \times z}$

## Proof

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

### Basis for the Induction

 $\displaystyle \left({x^y}\right)^0$ $=$ $\displaystyle 1$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle x^0$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle x^{y \mathop \times 0}$ definition of ordinal multiplication

This proves the basis for the induction.

$\Box$

### Induction Step

Suppose that $\left({x^y}\right)^z = x^{y \mathop \times z}$.

Then:

 $\displaystyle \left({x^y}\right)^{z^+}$ $=$ $\displaystyle \left({x^y}\right)^z \times x^y$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle x^{y \mathop \times z} \times x^y$ by Inductive Hypothesis $\displaystyle$ $=$ $\displaystyle x^{\left({y \mathop \times z}\right) + y}$ by Ordinal Sum of Powers $\displaystyle$ $=$ $\displaystyle x^{y \mathop \times z^+}$ definition of ordinal multiplication

This proves the induction step.

$\Box$

### Limit Case

Suppose $\left({x^y}\right)^w = x^{y \mathop \times w}$ for all $w \in z$ where $z$ is a limit ordinal.

Then:

 $\, \displaystyle \forall w \in z: \,$ $\displaystyle \left({x^y}\right)^w$ $=$ $\displaystyle x^{y \mathop \times w}$ by Inductive Hypothesis $\displaystyle \implies \ \$ $\displaystyle \bigcup_{w \mathop \in z} \left({x^y}\right)^w$ $=$ $\displaystyle \bigcup_{w \mathop \in z} x^{y \mathop \times w}$ by Indexed Union Equality $\displaystyle \implies \ \$ $\displaystyle \left({x^y}\right)^z$ $=$ $\displaystyle \bigcup_{w \mathop \in z} x^{y \mathop \times w}$ definition of ordinal exponentiation

To prove the statement, it is necessary and sufficient to prove that:

$\displaystyle \bigcup_{w \mathop \in z} x^{y \mathop \times w} = x^{y \mathop \times z}$

The proof of this shall proceed by cases:

#### Case 1

If $y = 0$, it follows that:

 $\displaystyle \left({x^y}\right)^z$ $=$ $\displaystyle 1^z$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle 1$ by Exponent Base of One $\displaystyle$ $=$ $\displaystyle x^0$ definition of ordinal exponentiation $\displaystyle$ $=$ $\displaystyle x^{y \mathop \times z}$ by Ordinal Multiplication by Zero

#### Case 2

If $y \ne 0$:

 $\displaystyle w$ $\in$ $\displaystyle z$ $\displaystyle \implies \ \$ $\displaystyle \left({y \mathop \times w}\right)$ $\le$ $\displaystyle \left({y \mathop \times z}\right)$ by Membership is Left Compatible with Ordinal Multiplication and Ordinal Multiplication by Zero $\displaystyle \implies \ \$ $\displaystyle x^{y \mathop \times w}$ $\le$ $\displaystyle x^{y \mathop \times z}$ by Membership is Left Compatible with Ordinal Exponentiation and definition of ordinal exponentiation

Therefore, by Supremum Inequality for Ordinals, it follows that:

$\bigcup_{w \mathop \in z} x^{y \mathop \times w} \le x^{y \mathop \times z}$

Conversely:

 $\displaystyle v$ $\in$ $\displaystyle y \times z$ $\displaystyle \implies \ \$ $\, \displaystyle \exists w \in z: \,$ $\displaystyle v$ $\in$ $\displaystyle y \times w$ by Ordinal is Less than Ordinal times Limit $\displaystyle \implies \ \$ $\displaystyle x^v$ $\le$ $\displaystyle x^{y \mathop \times w}$ by Membership is Left Compatible with Ordinal Exponentiation

By Supremum Inequality for Ordinals, it follows that:

$\displaystyle \bigcup_{v \mathop \in y \mathop \times z} x^v \le \bigcup_{w \mathop \in z} x^{y \mathop \times w}$

Therefore, by the definition of ordinal exponentiation:

 $\displaystyle x^{y \mathop \times z}$ $=$ $\displaystyle \bigcup_{w \mathop \in z} x^{y \mathop \times w}$ $\displaystyle$ $=$ $\displaystyle \left({x^y}\right)^z$

This proves the limit case.

$\blacksquare$