Strictly Increasing Mapping on Well-Ordered Class

This article needs to be linked to other articles. In particular: Both definitions and pages justifying the various steps in the argument. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

Theorem

Let $\struct {S, \prec}$ be a strictly well-ordered class.

Let $\struct {T, <}$ be a strictly ordered class.

Let $f$ be a mapping from $S$ to $T$.

For each $i \in S$ such that $i$ is not maximal in $S$, let:

$\map f i < \map f {\map \Succ i}$

where $\map \Succ i$ is the immediate successor element of $i$.

Let:

$\forall i, j \in S: i \preceq j \implies \map f i \le \map f j$

Then for each $i, j \in S$ such that $i \prec j$:

$\map f i < \map f j$

This article needs to be linked to other articles. In particular: In the above, link to definitions of increasing mapping and strictly increasing mapping, in order to correlate with page title. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

Proof

This page is beyond the scope of ZFC, and should not be used in anything other than the theory in which it resides.

If you see any proofs that link to this page, please insert this template at the top.

If you believe that the contents of this page can be reworked to allow ZFC, then you can discuss it at the talk page.

By Non-Greatest Element of Well-Ordered Class has Immediate Successor, $\map \Succ i$ is guaranteed to exist.

Let $i \prec j$.

Let $S_i := \set {q \in S: i \prec q}$.

This article, or a section of it, needs explaining. In particular: Important to specify what the domain of $q$ actually is -- presumably $S$. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code.

Then $\map \Succ i$ is the minimal element of $S_i$.

By supposition, $j \in S_i$.

Thus:

$j \nprec \map \Succ i$

Since Well-Ordering is Total Ordering:

$\map \Succ i \preceq j$

Thus by supposition:

$\map f {\map \Succ i} \le \map f j$

Since $\map f i < \map f {\map \Succ i}$:

$\map f i < \map f j$

by transitivity.

$\blacksquare$