Let $F$ denote the function $\lbrace (i,S_i) : i < \omega \rbrace$ in whatever sense it may exist---I hope this abuse of notation will not be confusing.

The undefinability of truth does "get in the way" in the sense that it shows that there cannot be such a function $F$ that is definable.
If we let $C$ be the set of $i$ such that $\sigma_i$ is a sentence ($x$ does not appear) then from $F$ we could define $\lbrace i \in C : S_i = \mathbb{R}\rbrace$, which is essentially a truth set and therefore cannot be definable by Tarski's theorem.

EDIT: it looks like I am using "definable" to mean "definable without parameters" and Joel is using it to mean "definable with parameters." As Joel points out in the comments and in his answer, it is *possible* for a truth set, and indeed the desired function $F$, to be definable from ordinal parameters.

To answer the precise question you stated, ZFC does not *prove* the existence of such a function $F$. As Andreas mentions in the comments to Bjørn's answer, there are models of ZFC in which all sets are definable. (This is not a first-order property of the model.) Any such model $M$ cannot satisfy "the desired function exists" regardless of how we try to formalize this. One way to see this is that if there were such a function $F \in M$, then externally we could use the fact that every set in $M$ is definable in $M$ to show that $ran(F) = \mathcal{P}(\mathbb{R})^M$. This statement about the range is absolute to $M$, contradicting Cantor's theorem in $M$.