Unique Ordinal Exponentiation Inequality

Theorem

Let $x$ and $y$ be ordinals.

Let $x > 1$ and $y > 0$.

Then there exists a unique ordinal $z$ such that:

$x^z \le y$ and $y < x^{z^+}$

Therefore, $y$ is bounded above by $x^w$ for some $w$, so there is a smallest $w$ such that:

Moreover, if $w$ is a limit ordinal then there is some $v ∈ w$ such that $y < x^v$, contradicting the fact that $w$ is minimal.

Therefore, $w$ is not a limit ordinal and therefore must be the successor of some ordinal.

So $w = z^+$ for some $z$.

Since $z < z^+$, it follows that $x^z ≤ y$ and $y < x^{z^+}$.

$\Box$

Assume that $x^z \le y$ and $y < x^{z^+}$ for some $z = z_1$ and $z = z_2$.

Then $x^{z_1} < x^{z_2^+}$ and $x^{z_2} < x^{z_1^+}$.

Similarly $z_2 \le z_1$.

By definition of set equality:

$z_1 = z_2$

$\blacksquare$