Initial Segment of Canonical Order is Set

From ProofWiki
Jump to navigation Jump to search



Theorem

Let $R_0$ denote the canonical ordering of $\paren {\On \times \On}$.

Then, for all $\tuple {x, y} \in \paren {\On \times \On}$, the $R_0$-initial segment is a set.




Proof

Let $z = \map \max {x, y}^+$.

Let $\tuple {v, w} \mathrel R_0 \tuple {x, y}$.


Then:

\(\ds \map \max {v, w}\) \(\le\) \(\ds \map \max {x, y}\)
\(\ds \) \(\lt\) \(\ds z\)

Thus, the initial segment:

$\paren {\On \times \On}_{\tuple {x, y} } \subseteq \paren {z \times z}$



By Axiom of Subsets Equivalents, the initial segment of $\tuple {x, y}$ is a set.

$\blacksquare$


Sources