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 relation $\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

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

The conclusion:

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

follows from propositional logic.

Inductive Case

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

Limit Case

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