You can formalize
The initial function you mention is the question as diagonalizingfunction $d:\mathbb{R}^\omega\to\mathbb{R}$, for which oneensures that $z=d(x_0,x_1,\ldots)$ is distinctfrom every $x_n$ simply by making the assertion $n$-th digit of $z$different from the $n$-th digit of $x_n$ in some regularway. Since the graph of this function is arithmeticallydefinable (needing to look only at the individual digitsof the input and output), it follows that there$d$ is no a Borelfunctiondefined .
The point of your question, however, is that this function is notwell-defined on sequences to realsdifferent enumerations of the same set---the resulting diagonal value will be different if you rearrange the input.What would be desired is a function$f:\mathbb{R}^\omega\to\mathbb{R}$ such that always$f(x_0,x_1,\ldots)\neq x_n$, but for which always $f$ gives thesame value to all for different enumerations of the same set, and which gives a value outside the given countableset. Suppose towards contradiction Unfortunately, there is no such function that isBorel.
Theorem. There is no Borel function$f:\mathbb{R}^\omega\to\mathbb{R}$ has this feature such that
Proof.
(Such The nonexistence of such a function is closely related in spirit, in thecontext of Borel equivalence relation theory, to thepossibility impossibility of a Borel reduction of from the equivalence relation$E_{set}$ to $=$, in the context of Borel equivalence relation theory, and this the argument below belongs to thattheory.)
Continuing with the subject. The argument will use set-theoretic forcing, let$\mathbb{P}$ be the partial andis an instance where forcing is used in order consisting of all finitesequences of real numbersto make aconclusion about the ground model $V$, rather than to prove anindependence result.
To begin, ordered suppose that $f$ is a Borel function with longer sequenceslower in the ordertwoproperties. This is Let $\mathbb{P}=\text{Coll}(\omega,\mathbb{R})$be the usual forcing notion to collapse $\mathbb{R}$ to $\omega$, and the \omega$. Thatis, conditions in $\mathbb{P}$ are finite sequences ofreals, ordered by end-extension. The generic object will beground model $V$. Let $g_0$ g$ and $g_1$ h$ be mutually $V$-genericextensions $V[g_0]$, V[g]$, $V[g_1]$ V[h]$ and their common extension$V[g_0][g_1]$. V[g][h]$. Since $f$ was a Borel function, it has a Borelis a $\Sigma^1_2$ \Pi^1_1$ statement about this Borel code, and henceabsolute between $V$ and these larger universes. That is,the re-interpreted function $f$ continues to have thedesired properties in $V[g][h]$. Since $g_0$ g$ and $g_1$ h$ bothenumerate the same set $\mathbb{R}^V$, it follows that$f(g_0)=f(g_1)$ f(g)=f(h)$ in $V[g_0][g_1]$. V[g][h]$. In particular, the value$z=f(g_0)$ z=f(g)=f(h)$ is in both $V[g_0]$ V[g]$ and $V[g_1]$. V[h]$. But since $g_0$ g$and $g_1$ h$ are mutually generic, it follows that $V[g_0]\cap V[g_1]=V$V[g]\capthat $f(g_0)$ f(g)$ should be a real not listed in $g_0$, g$, since $g_0$ g$
The practitioners of Borel equivalence relation theory havea large bag of tools at their disposal---many argumentsproceed with one's choice of forcing or ergodic theory andgroup actions or something else---and I expect similarlythat there is a forcing-free proof of the theorem above(perhaps someone can post such an argument?). But to my way of thinking, theforcing proof is fairly sharp.
Lastly, let me say that if there are sufficient largecardinals, then projective truth is absolute from $V$ to$V[g][h]$, and in this case, the same argument shows thatthere can be no projective function $f$ with the twoproperties. Since the Borel functions sit merely at thedoorstep of the projective hierarchy, this would be anenormous expansion of the phenomenon.

