Membership is Left Compatible with Ordinal Multiplication

From ProofWiki
Jump to navigation Jump to search


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


$\left({ x < y \land z > 0 }\right) \iff \left({ z \cdot x }\right) < \left({ z \cdot y }\right)$


Sufficient Condition

The proof of the sufficient condition shall proceed by Transfinite Induction on $y$.

Basis for the Induction

Both $x < 0$ and $\left({ x \cdot z }\right) < \left({ 0 \cdot z }\right)$ are contradictory, so the iff statement holds for the condition that $y = 0$.

This proves the basis for the induction.

Induction Step

Suppose the biconditional statement holds for $y$. Then:

\(\displaystyle x < y^+\) \(\implies\) \(\displaystyle x < y \lor x = y\) Definition:Successor Set
\(\displaystyle x < y \land z > 0\) \(\implies\) \(\displaystyle \left({ z \cdot x }\right) < \left({ z \cdot y }\right)\) Inductive Hypothesis
\(\displaystyle x = y\) \(\implies\) \(\displaystyle \left({ z \cdot x }\right) = \left({ z \cdot y }\right)\) Leibniz's law
\(\displaystyle z > 0\) \(\implies\) \(\displaystyle \left({ z \cdot y }\right) < \left({ \left({ z \cdot y }\right) + z }\right)\) Membership is Left Compatible with Ordinal Addition
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ z \cdot y }\right) < \left({ z \cdot y^+ }\right)\) Definition:Ordinal Multiplication
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ z \cdot x }\right) < \left({ z \cdot y^+ }\right)\) Transitivity of $<$ and Leibniz's law

In either case, $\left({ z \cdot x }\right) < \left({ z \cdot y^+ }\right)$

This proves the induction step.

Limit Case

Suppose $y$ is a limit ordinal:

\(\displaystyle \) \(\) \(\displaystyle \forall w \in y: \left({ \left({ x < w \land z > 0 }\right) \iff \left({ z \cdot x }\right) < \left({ z \cdot w }\right) }\right)\) Hypothesis
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ \exists w \in y: \left({ x < w \land z > 0 }\right) \iff \exists w \in y: \left({ z \cdot x }\right) < \left({ z \cdot w }\right) }\right)\) Predicate Logic Manipulation
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ \left({ x < \bigcup y \land z > 0 }\right) \iff \left({ z \cdot x }\right) < \bigcup_{w \mathop \in y} \left({ z \cdot w }\right) }\right)\) Definition of Set Union
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ \left({ x < y \land z > 0 }\right) \iff \left({ z \cdot x }\right) < \bigcup_{w \mathop \in y} \left({ z \cdot w }\right) }\right)\) Union of Limit Ordinal
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ \left({ x < y \land z > 0 }\right) \iff \left({ z \cdot x }\right) < \left({ z \cdot y }\right) }\right)\) Definition of Ordinal Multiplication

This proves the limit case.

Necessary Condition

Conversely, suppose $\left({ z \cdot x }\right) < \left({ z \cdot y^+ }\right)$.

Then $z \ne 0$ because if it were equal, both sides of the inequality would be $0$.

So $z > 0$.


$y < x \implies \left({ z \cdot y }\right) < \left({ z \cdot x }\right)$
$y = x \implies \left({ z \cdot y }\right) = \left({ z \cdot x }\right)$

So if $\left({ z \cdot x }\right) < \left({ z \cdot y }\right)$, then $y \ne x$ and $y \not < x$, so $x < y$ by Ordinal Membership is Trichotomy.