Subset is Right Compatible with Ordinal Exponentiation

From ProofWiki
Jump to navigation Jump to search


This article needs to be linked to other articles.
In particular: link 'right compatible', 'induction hypothesis'
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.


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 = \O$, then $x^z = 1$

\(\ds x^z\) \(=\) \(\ds 1\) Definition of Ordinal Exponentiation
\(\ds y^z\) \(=\) \(\ds 1\) Definition of Ordinal Exponentiation
\(\ds x^z\) \(\le\) \(\ds 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:

\(\ds x^{z^+}\) \(=\) \(\ds x^z \times x\) Definition of Ordinal Exponentiation
\(\ds \) \(\le\) \(\ds x^z \times y\) Membership is Left Compatible with Ordinal Multiplication
\(\ds \) \(\le\) \(\ds y^z \times y\) Subset is Right Compatible with Ordinal Multiplication
\(\ds \) \(=\) \(\ds 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.


\(\ds \forall w \in z: \, \) \(\ds x^w\) \(\subseteq\) \(\ds y^w\) Inductive Hypothesis
\(\ds \leadsto \ \ \) \(\ds \bigcup_{w \mathop \in z} x^w\) \(\subseteq\) \(\ds \bigcup_{w \mathop \in z} y^w\) Indexed Union Subset
\(\ds \leadsto \ \ \) \(\ds x^z\) \(\subseteq\) \(\ds y^z\) Definition of Ordinal Exponentiation

This proves the limit case.

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Subset_is_Right_Compatible_with_Ordinal_Exponentiation&oldid=537112"