Construct the embedding of a subset of a well-order to the full set

Question

I'm trying to build the theory of well-orders without mentioning ordinals. Define a map $f : X \to Y$ between well-ordered sets to be a simulation, if it is an order equivalence (i.e. for all $x_0, x_1 \in X$, $x_0 < x_1 \iff f(x_0) < f(x_1)$) and its image is downwards-closed (i.e. for all $x_0 \in X, y \in Y$ with $y < f(x_0)$ there is some $x \in X$ with $y = f(x)$). Then there is a simulation $X \to Y$ iff the ordinals corresponding to $X$ is included in the ordinal corresponding to $Y$. Such maps are uniquely determined if they exist.

Now consider a well-ordered set $\langle X, <\rangle$ and a subset $U \subseteq X$. There is an induced well-order $<_U$ on $U$, defined by $<_U := < \cap U^2$. From the theory using ordinals, we know that the ordinal of $U$ is included in the ordinal of $X$. But how to prove this without ordinals, the map has to be written down explicitly.

I claim the following map is the right one. Define $f : U \to X$ recursively as $$ f(x) := \sup \{ f(y)^+ \mid y <_U x \}. $$

In this formula, $x^+$ denotes the successor of $x$ in the order $<$ (i.e. the smallest element strictly larger than $x$). I managed to show that this map is well-defined and an order-equivalence. But I didn't manage to prove that its image is downwards-closed and would appreciate some help.

Approaches

I expect that some inductive argument is necessary, but I didn't find it yet. Some things I thought about:

• If we can show that $w = sup \{ f(y)^+ \mid y <_U x \}$ iff $x = \sup \{ u^{+_U} \mid f(u) < w \}$, then it works out. (Here we need $u^{+_U} \in U$ to be the successor of $u \in U$ with respect to $<_U$.) We can and need to assume that $w < f(x_0)$ for some $x_0 \in U$, because otherwise (if $U$ has too few elements, e.g. if $w$ is larger than any element of $U$) it won't work.
• Using proof by contradiction we can reformulate the problem to the following. “Let $y \in X$ be an element which is not in the image of $f$. Now show that it is an upper bound for the image of $f$.”
• I did manage to show that $f(x^+) = f(x)^+$ in the following sense: for all $x_0, x_1 \in U$, $x_1$ is the successor of $x_0$ (w.r.t $<_U$) iff $f(x_1)$ is the successor of $f(x_0)$ (w.r.t. $<$).

Answer 1

Given a well-order $V$ and some $x \in V$, let $[, x]_V$ denote the well-ordered set $\{y \in V \mid y \leq x\}$. Note that the inclusion $[, x]_V \subseteq V$ is a simulation. Note also that the composition of simulations is a simulation.

Prove the following “gluing property”: suppose for all $c \in V$, there is a simulation $[,c]_V \to X$. Then there is a simulation $V \to X$.

We prove that for all $x \in U$, there is some simulation $[, x]_U \to [,x]_X$. This can be done using the gluing property and induction.

From here, note that we have simulations $[,x]_U \to [,x]_X \to X$. By the gluing property, we have a simulation $U \to X$.

Answer 2

I found an alternate but more technical solution. I use proof by contradiction and the law of trichotomy a lot.

Consider a minimal element $y \in X$ not in the image of $f$ and show that it is an upper bound for the image of $f$. So consider an arbitrary element $x \in U$ and show that $f(x) ≤ y$. Assume for a contradiction, that $y < f(x)$. Then we can replace $x$ by a minimal element of $U$ with the property that $y < f(x)$. By definition $f(x) = \sup \{f(z)^+ \mid z <_U x\}$, so if $y$ is an upper bound to this set, then (by def. of the supremum) $f(x) \le y$ and we have a contradiction.

For this, take $z <_U x$ and now show that $f(z)^+ \le y$.

Assume the contrary, i.e. that $y < f(z)^+$. Note that $f(z) < y$, because otherwise either $y$ lies in the image of $f$ or the minimality of $x$ is contradicted. This makes $y$ an element between $f(z)$ and its successor, which is impossible, ending the proof.