Subset is Right Compatible with Ordinal Exponentiation

From ProofWiki
Jump to navigation Jump to search

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$


Sources