# Membership is Left Compatible with Ordinal Multiplication

## Theorem

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

Then:

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

## Proof

### 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$.

Furthermore:

$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.

$\blacksquare$