Every countable linear order embeds in the rationals

If $L=\mathrm{\varnothing }$, the empty function is the required injection. Hence assume $L\mathrm{\ne }\mathrm{\varnothing }$; by [F2] fix a surjection $e:\mathbb{N}\to L$, and by [F3] fix a bijection $\rho :\mathbb{N}\to \mathbb{Q}$. These are two witnesses to two existential statements, not a simultaneous choice from a family.

Put $L_n=e[\{k:k<n\}]$. Suppose $f_n:L_n\to \mathbb{Q}$ is strictly order preserving and put $x=e(n)$. If $x\mathrm{\notin }{L}_n$, the already placed points below and above $x$ have finite image sets $B_n=\{f_n(y):y\in L_n,y{<}_{L}x\}$ and $C_n=\{f_n(y):y\in L_n,x{<}_{L}y\}$. Induction on the finite list $e(0),\dots ,e(n-1)$ and totality give a maximum $b$ of $B_n$ when it is nonempty and a minimum $c$ of $C_n$ when it is nonempty; strict preservation gives $b<c$ when both exist. Thus the set $I_n$ of rationals strictly above $b$ and below $c$, with either missing constraint omitted, is nonempty: use $(b+c)\mathrm{/}2$ when both exist, $b+1$ or $c-1$ when just one exists, and $0$ when neither exists. Every old point is below or above $x$ by linearity, so every member of $I_n$ is outside $f_n[L_n]$.

Apply recursion to states $(n,f_n)$, starting with $(0,\mathrm{\varnothing })$ and incrementing the first coordinate at each transition. Given $f_n$, leave it unchanged when $e(n)\in L_n$, and otherwise let $m_n=\min \{m:\rho (m)\in I_n\}$ and put $f_{n+1}=f_n\cup \{(e(n),\rho (m_n))\}$. The set minimized over is nonempty by step 1.2 and surjectivity of $\rho$, so [F7] makes the state transition single-valued. Induction using step 1.2 shows that every $f_n$ is a function with domain $L_n$, extends every earlier $f_k$, and is strictly order preserving.

Let $f={\bigcup }_{n\in \mathbb{N}}{f}_n$. Coherence makes $f$ a function. For each $x\in L$, surjectivity of $e$ makes $\{n:e(n)=x\}$ nonempty, so its least member $k$ exists by [F7] and $x\in L_{k+1}$; hence $\mathrm{dom}(f)=L$. If $x{<}_{L}y$, choose stages containing both; a later common stage exists and its strict preservation gives $f(x)<f(y)$. Thus $f$ is strictly order preserving, and therefore injective: for distinct $x,y$, linearity gives one of $x{<}_{L}y$ or $y{<}_{L}x$, so their images are distinct.

The empty case and step 3.1 prove the theorem for every at most countable linear order. The only selections were the two fixed existential witnesses $e,\rho$; every later rational was determined by a least natural index, so the construction is valid in ZF and uses no form of the Axiom of Choice.