How to formalize the below solution

Yes, this can be made precise (and true)! I would attack it as follows.

It will be helpful to introduce some terminology. Let's say that a trail is a pair of sequences $$\mathfrak{t}=\langle(a_i)_{i<\alpha}, (b_j)_{j<\alpha}\rangle$$ indexed by some ordinal $\alpha$ such that $a<a_i<a_{i+1}<b_{i+1}<b_i<b$ and $f(a_i)=f(b_i)$ for all $i<\alpha$. There is an obvious notion of extension of trails, and since the union of a chain of trails is again a trail Zorn's lemma tells us that there exists a (presumably non-unique!) non-"extendible" trail $\mathfrak{s}=\langle (u_i)_{i<\gamma},(v_i)_{i<\gamma}\rangle$. (changing up notation slightly to avoid possible mix-ups).

Now consider the sets $U=\{u_i:i<\gamma\}, V=\{v_i:i<\gamma\}$. These are bounded above and below respectively (in fact each is bounded both above and below), so by the completeness of $\mathbb{R}$ we have that $y:=\sup(U)$ and $z:=\inf(V)$ each exist. Clearly $y\le z$, and by continuity of $f$ we have $f(y)=f(z)$, but since $\mathfrak{s}$ is appropriately maximal we must not be able to "tack on" $y$ and $z$ to the left and right components of $\mathfrak{s}$ respectively to get a longer trail. This means that we must have $y=z$; let's take this point to be our $x$.

Now we need to extract a pair of length-$\omega$ sequences leading to $x$ from below and from above. The components of the maximal trail $\mathfrak{s}$ probably won't do, since the length of $\alpha$ might be much longer than $\omega$. However, it's at this point that a general topology fact comes into play:

$(*)\quad$ There is no order-preserving (or order-reversing) embedding of an uncountable ordinal into $\mathbb{R}$.

Consequently, the length $\gamma$ of $\mathfrak{s}$ must be a countable ordinal. Combined with the argument implicit in your post that this length must be a limit ordinal, we can extract a cofinal-in-$\gamma$ length-$\omega$ sequence $(\theta_i)_{i<\omega}$ of ordinals $<\gamma$; we'll then just set $$a_i=u_{\theta_i},\quad b_i=v_{\theta_i}.$$

Of course we still have to prove $(*)$, but this is a good exercise (think about how the countable set $\mathbb{Q}$ "sits inside" $\mathbb{R}$).

As a quick aside, my use of Zorn's lemma is - unsurprisingly - unnecessary, although it does simplify things. It's a fun, or perhaps "fun," exercise to modify the argument above so that no appeal to choice is used: by some cleverness involving $\mathbb{Q}$ we can actually build an explicit(ish) maximal trail, given appropriate $a,b,f$.