The theorem:
Let $X$ be a totally ordered set (with at least two elements) such that for every $x < y$, there's a $z$ that lies between the two. Then for any $a < b$, there exists an order-preserving injection $\mathbb Q\to (a, b)$.
The proof presented went as follows:
First, we arrange $\mathbb Q$ as $\{q_1, q_2, \ldots\}$ for distinct $q_i$'s. We define a function $\eta\colon \mathbb Q\to (a, b)$ as follows. First we choose $\eta(q_1)\in (a, b)$. Then assuming that we have chosen $\eta(q_i)$'s in $(a, b)$ in an order-preserving manner for all $i\le n$, we can choose the next $\eta(q_{n+1})$ in the following manner.
- If $q_{n+1}$ lies between $q_i$ and $q_j$ (such that no other $q_k$ is between them) then we choose $\eta(q_{n+1})$ between $\eta(q_i)$ and $\eta(q_j)$.
- If $q_{n+1}$ is less than all $q_i$'s, then we choose $\eta(q_{n+1})$ between $a$ and $\min_{1\le i\le n}\eta(q_i)$.
- If $q_{n+1}$ is greater than all $q_i$' then we choose $\eta(q_{n+1})$ between $\max_{1\le i\le n}\eta(q_i)$ and $b$.
This proof clearly has some flavor of choice in it. However, how to formalize it precisely?
We use dependent choice.
Consider the set $\mathcal S$ comprising of the order-preserving $\eta\colon \{q_1, \ldots, q_n\}\to (a, b)$ for $n\ge 1$. Then define a relation $R$ on $\mathcal S$ as $$ (\eta, \xi)\in R\iff \text{$\xi$ is a strict extension of $\eta$.} $$
Then $R$ is a total relation on $\mathcal S$. (Reason is similar to that provided in the proof in the post.) Thus by dependent choice, we can consider a sequence $(\eta_1, \eta_2, \ldots)$ of order-preserving injections from finite initial segments of $\{q_1, q_2, \ldots\}$ into $(a, b)$ where each $\eta_{i+1}$ is a strict extension of $\eta_i$.
Now we can define an $\eta\colon\mathbb Q\to (a, b)$ by $$ \eta(q_i) := \eta_i(q_i)\text. $$ (The domain of $\eta_i$ contains at least $\{q_1, \ldots, q_i\}$.)
It is now easy to show that this $\eta$ preserves order.