Let $V \models ZFC$. Let $P$ be a forcing and $G \subseteq P$ be generic over $V$. Let $x \in V[G]$.
Let $M$ be the class of set that are hereditarily definable (in $V[G]$) using as parameters $x$ and elements of the ground models $V$.
I would like to know if $M$ satisfies Axiom of Choice.
I believe this $M$ is the same as $HOD^{V[G]}(V \cup \{x\})$ as the ordinals of $V[G]$ are already in $V$. The one single elements $x$ as parameter should not affect whether $M$ models choice. (The same reason why $HOD[x]$ always satisfy choice.) So I believe this question is equivalent to whether $HOD^{V[G]}(V)$ satisfies the axiom of choice.
The meaning of parenthesis and bracket above refer to Jech's convention. Thanks for any help.
You can do the following: for each $A\in HOD^{V[G]}(V)$, let $\beta\in Ord$ be large enough such that $V_\beta$ contains all parameters in the hereditary definition of $A$. Fix a well ordering of $V_\beta$ in $V$, say $\prec$. Now we attempt to define an injection from $A$ to $ORD$ in $V[G]$ that is ordinal definable with parameter $\prec \in V$. Let $\gamma=type(\prec)$ and consider $A\to \omega\times (\gamma)^{<\omega}$ such that $a\in A$ is mapped to the least (some well ordering of $\omega\times (\gamma)^{<\omega}$ and by standard argument it is OD) $(\varphi, \gamma_0, \cdots,\gamma_n)$ such that $a$ is defined by $\varphi(a, \prec(\gamma_0),\cdots, \prec(\gamma_n))$ in $V[G]$ where $\prec(\gamma_i)$ is the $\gamma_i$-th element in the well ordering $\prec$. Clearly this is injective and $OD^{V[G]}(V)$ but as $A\times (\omega\times (\gamma)^{<\omega})\subset HOD^{V[G]}(V)$ we know this injection is actually in $HOD^{V[G]}(V)$. Done.