Membership is Left Compatible with Ordinal Addition

From ProofWiki
Jump to navigation Jump to search


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

Let $<$ denote membership $\in$, since $\in$ is a strict well-ordering on the ordinals.


$x < y \implies \paren {z + x} < \paren {z + y}$


The proof proceeds by transfinite induction on $y$.

In the proof, we shall use $\in$, $\subsetneq$, and $<$ interchangeably.

We are justified in this by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.

Base Case

\(\displaystyle \neg x\) \(=\) \(\displaystyle \O\) Definition of Empty Set

The conclusion:

$x < \O \implies \paren {z + x} < \paren {z + \O}$

follows from propositional logic.

Inductive Case

\(\displaystyle x < y\) \(\leadsto\) \(\displaystyle \paren {z + x} < \paren {z + y}\) Hypothesis
\(\displaystyle x < y^+\) \(\leadsto\) \(\displaystyle x < y \lor x = y\) Definition of Successor Set
\(\displaystyle \paren {z + y^+} = \paren {z + y}^+\) \(\) \(\displaystyle \) Definition of Ordinal Addition
\(\displaystyle \paren {z + y} < \paren {z + y^+}\) \(\) \(\displaystyle \) Ordinal is Less than Successor
\(\displaystyle x < y\) \(\leadsto\) \(\displaystyle \paren {z + x} < \paren {z + y^+}\) Hypothetical Syllogism
\(\displaystyle x = y\) \(\leadsto\) \(\displaystyle \paren {z + x} < \paren {z + y^+}\) Substitutivity of Equality
\(\displaystyle x < y^+\) \(\leadsto\) \(\displaystyle \paren {z + x} < \paren {z + y^+}\) Proof by Cases

Limit Case

\(\displaystyle \) \(\) \(\displaystyle \forall w < y: \paren {x < w \implies \paren {z + x} < \paren {z + w} }\)
\(\displaystyle \) \(\leadsto\) \(\displaystyle \paren {\exists w < y: x < w \implies \exists w < y \paren {z + x} < \paren {z + w} }\) Predicate Logic Manipulation
\(\displaystyle \) \(\leadsto\) \(\displaystyle \paren {x < y \implies \paren {z + x} < \bigcup_{w \mathop \in y} \paren {z + w} }\) Membership of Indexed Union
\(\displaystyle \) \(\leadsto\) \(\displaystyle \paren {x < y \implies \paren {z + x} < \paren {z + y} }\) Definition of Ordinal Addition