Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into $\mathbb{N}$ being built from one fixed enumeration of the rationals by least index, so no choice principle is used

First prove the construction for a nondecreasing function and any fixed rational enumeration $e$. For an original nonincreasing $f$, apply that construction to $-f$ with the reflected enumeration $k\mapsto -e(k)$. The one-sided limits of $-f$ are $-L^{-}(c)$ and $-L^{+}(c)$, with their side labels unchanged, directly from the absolute-value limit condition. Hence $-L^{-}(c)<-e(k)<-L^{+}(c)$ holds exactly when $L^{+}(c)<e(k)<L^{-}(c)$. The least indices for the transformed upward gap and the original ordered gap therefore agree. The discontinuity set is unchanged, and the endpoint codes depend only on $I$, so the resulting injection has exactly the stated form. Assume from here on that $f$ is nondecreasing.

Fix once and for all a bijection $e:\mathbb{N}\to {\mathbb{Q}}_{\mathbb{R}}$; everything below is defined in terms of $f$, $I$ and this one function.

Call $c\in I$ interior when both $I^{-}$ and $I^{+}$ are nonempty, and write $D_0$ for the set of interior points of $I$ at which $f$ is discontinuous. A point of $I$ that is not interior has $I^{-}=\mathrm{\varnothing }$, and is then a least element of $I$, or $I^{+}=\mathrm{\varnothing }$, and is then a greatest element of $I$; a subset of $\mathbb{R}$ has at most one least and at most one greatest element, so $D\setminus D_0$ has at most two elements.

For $c\in D_0$ put $L^{-}(c):={\lim }_{x\to c^{-}}f(x)$ and $L^{+}(c):={\lim }_{x\to c^{+}}f(x)$, both of which exist, and note $L^{-}(c)<L^{+}(c)$.

Let $c,c^{\mathrm{\prime }}\in D_0$ with $c<c^{\mathrm{\prime }}$. Take $t:=e(k)$ for the least $k$ with $c<e(k)<c^{\mathrm{\prime }}$, which exists because a point of ${\mathbb{Q}}_{\mathbb{R}}$ lies strictly between $c$ and $c^{\mathrm{\prime }}$; then $t\in I$, since $c,c^{\mathrm{\prime }}\in I$ and $I$ is order-convex.

For $c\in D_0$ the set $K(c):=\{k\in \mathbb{N}:L^{-}(c)<e(k)<L^{+}(c)\}$ is nonempty, since a point of ${\mathbb{Q}}_{\mathbb{R}}$ lies strictly between the two distinct reals $L^{-}(c)$ and $L^{+}(c)$ and $e$ is onto ${\mathbb{Q}}_{\mathbb{R}}$; so $j(c):=\min K(c)$ is a well-defined natural number, determined by $c$, $f$ and $e$ alone.

With $c<t<c^{\mathrm{\prime }}$ as in step 2.2: $L^{+}(c)=\inf \{f(x):x\in I,x>c\}\le f(t)$ because $t$ is one of the points in that set, and $f(t)\le \sup \{f(x):x\in I,x<c^{\mathrm{\prime }}\}=L^{-}(c^{\mathrm{\prime }})$ for the same reason on the other side. Hence $L^{+}(c)\le L^{-}(c^{\mathrm{\prime }})$.

The two open intervals $(L^{-}(c),L^{+}(c))$ and $(L^{-}(c^{\mathrm{\prime }}),L^{+}(c^{\mathrm{\prime }}))$ are therefore disjoint, so no point of ${\mathbb{Q}}_{\mathbb{R}}$ lies in both, so $e(j(c))\mathrm{\ne }e(j(c^{\mathrm{\prime }}))$ and hence $j(c)\mathrm{\ne }j(c^{\mathrm{\prime }})$. Since $c<c^{\mathrm{\prime }}$ was an arbitrary pair of distinct elements of $D_0$, the map $j:D_0\to \mathbb{N}$ is injective.

Define $J:D\to \mathbb{N}$ by $J(c):=2j(c)+1$ for $c\in D_0$; $J(c):=0$ if $c\in D\setminus D_0$ is a least element of $I$; and $J(c):=2$ if $c\in D\setminus D_0$ is a greatest element of $I$ and not a least one. Then $J$ is injective: it is injective on $D_0$ by step 4.1, it separates the at most two points of $D\setminus D_0$ from each other, and its values on $D_0$ are odd while its values off $D_0$ are even.

Consequently $J$ is a bijection from $D$ onto the subset $J[D]\subseteq \mathbb{N}$, which is at most countable; countability transfers along that bijection, so $D$ is at most countable.