Showing that $\mathsf{HOD}(\mathbb{R})$ always satisfies the axiom of countable choice This is exercise IV 8.12 in Kunen's set theory. $\mathsf{HOD}(\mathbb{R})$ denotes the class of sets hereditarily definable from finitely many ordinals and finitely many reals. Work in ZFC, and let $(E_n\mid n\in\omega)$ be in $\mathsf{HOD}(\mathbb{R})$. Then it is claimed that there is a choice function on the $E_n$'s in $\mathsf{HOD}(\mathbb{R})$.
Since we work in ZFC, there is a choice function for the $E_n$'s in $V$, and any such choice function is a subset of $\mathsf{HOD}(\mathbb{R})$. I think the approach to the exercise is to find some way to code the definitions of the countably many $f(E_n)$ by a single real? I am not really sure and I'd like to ask for help. Thank you.
 A: Since being ordinal-definable is expressible, we write $D(\alpha,x)=y$ if and only if $\alpha$ codes a finite sequence of ordinals, the first one coding a formula, which, along with the rest of that sequence and $x$ as parameters, defines $y$.
Now let $(E_n\mid n\in\omega)$ be as in the question (assume none of them is empty, of course). Working in $V$ where we have $\mathsf{ZFC}$, we are going to inductively define a function $f:\omega\to \mathsf{HOD}(\mathbb{R})$, and we will show that this $f$ is itself definable from ordinals and reals.
First, let $f(0)$ be some element of $E_0$. Let $\alpha_0$ be the least ordinal such that there is some $x\in \mathbb R$ such that $D(\alpha_0,x)=f(0)$. And let $x_0\in \mathbb R$ be a witness.
Now suppose $f(n),\alpha_n,x_n$ are defined. Let $\alpha_{n+1}$ be the least ordinal $\alpha$ such that there is some real $x$ with $D(\alpha,x)\in E_{n+1}$, let $x_{n+1}$ be a real witnessing this. Now let $f(n+1)=D(\alpha_{n+1},x_{n+1})$.
So we've defined a function $f:\omega\to\mathsf{HOD}(\mathbb{R})$. Since we have AC in $V$, we also have the sequence $(x_n\mid n\in\omega)$. Now let $r$ be a single real coding this sequence. Then we observe that the inductive definition of $f$ can be carried out with $r, \alpha_0, x_0$ as parameters. (Note that one need not worry about the sequence of the $\alpha_n$'s, since these are inductively obtained from $f_{n-1}$'s).
This shows that $f\in \mathsf{HOD}(\mathbb{R})$. A choice function for the $E_n$'s is easily obtained from $f$.
Finally, observe that this proof really shows the stronger result that $\mathsf{HOD}(\mathbb{R})\vDash \mathsf{DC}$. The relevant modification needed is to pick $\alpha_{n+1}$ to be least $\alpha$ such that there is some $x$ with $(f(n), D(\alpha,x))\in R$ for the given dependent relation $R$.
