Ordinal Power of Power

From ProofWiki
Jump to navigation Jump to search

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$


Sources