The answer is that we can't write a formula which provably defines a well-ordering of $\Bbb R$ in $\sf ZFC$ (at least assuming that $\sf ZFC$ is consistent), although I don't know whose to credit for it.
Suppose that $\varphi(x,y)$ provably defines a bijection of $\Bbb R$ with an ordinal (this is equivalent to the way you state it, just making it easier to work with later on). Note that $\sf ZF$ proves that every well-ordering has a unique isomorphism with a unique ordinal, so it doesn't depend on anything.
Let $M$ be a countable transitive model [of enough axioms] of $\sf ZFC$. Consider the forcing which adds one Cohen real. The conditions of this forcing are finite functions $p\colon\omega\to2$ (here we mean partial functions, of course), ordered by reverse inclusion.
Denote by $\dot c=\{(p,\check k)\mid p(k)=1\}$ the canonical name for the Cohen real. Let $G$ be an $M$-generic filter, and let $c$ denote the interpretation of our Cohen real by $G$.
In $M[G]$ there is some $\alpha$ such that $M[G]\models\varphi(c,\alpha)$, therefore for some $p\in G$ we have that $p\Vdash\varphi(\dot c,\check\alpha)$.
Now pick any $m,n\notin\operatorname{dom}(p)$ and consider the permutation of $\omega$ which is the cycle $(m\ n)$. This permutation is in $M$, and we can apply it to the conditions of the forcing (by the action $\pi p(\pi n)=p(n)$). So we can think of it as an automorphism of the forcing. Some basic facts:
- An automorphism of the forcing extends uniquely to an automorphism of the names.
- $p\Vdash\phi(\dot x)$ if and only if $\pi p\Vdash\phi(\pi\dot x)$ for an automorphism $\pi$.
- In the Cohen forcing, if $\pi$ is an automorphism induced as above by a permutation of $\omega$, and it is not the identity automorphism, then $1\Vdash\pi\dot c\neq\dot c$.
- If $x\in M$, then $\pi\check x=\check x$, where $\check x$ is the canonical name for $x$.
We now have that $\pi p\Vdash\varphi(\pi\dot c,\pi\check\alpha)$. But $\pi p=p$, and therefore $p\Vdash\varphi(\pi\dot c,\check\alpha)$. Which is a contradiction since now $p\Vdash\varphi\text{ defines an injective function}\land\pi\dot c\neq\dot c\land\varphi(\dot c,\check\alpha)\land\varphi(\pi\dot c,\check\alpha)$.