I've found out that what I'm looking for is what proposition implies $\exists y\;\forall x:(f(x)<y\lor y<f(x))$ and by definition $f(x)<y\lor y<f(x)\longleftrightarrow y\neq f(x)$ so there must exist an element in the codomain not in the image of $f$, so $f$ must not be surjective.
Supposing we don't know the definition of $a\neq b$:
$$X\implies\exists y\;\forall x:(f(x)<y\lor y<f(x))$$
taking the contrapositive
$$\lnot\exists y\;\forall x:(f(x)<y\lor y<f(x))\implies \lnot X$$
We found that the inverse of everything that $\lnot\exists y\;\forall x:(f(x)<y\lor y<f(x))$ implies is an answer. Simplifying the formula
\begin{align}
\lnot\exists y\;\forall x&:(f(x)<y\lor y<f(x))\\
\forall y\;\lnot\forall x&:(f(x)<y\lor y<f(x))\\
\forall y\;\exists x&:\lnot(f(x)<y\lor y<f(x))\\
\forall y\;\exists x&:(\lnot(f(x)<y)\land\lnot( y<f(x)))\\
\forall y\;\exists x&:(f(x)\leq y\land y\leq f(x))\\
\forall y\;\exists x&:y=f(x)\\
\end{align}
Inverting this we get
\begin{align}
\lnot\forall y\;\exists x&:y=f(x)\\
\exists y\;\lnot\exists x&:y=f(x)\\
\exists y\;\forall x&:y\neq f(x)\\
\end{align}
So this there must exists a number in the codomain that is not in the image of $f$, hence $f$ must not be surjective.