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$.