Cohen's first nonAC model, the one with a Dedekindfinite infinite set $A$ of reals, can be defined in two ways, 1st, as $HOD(A)$ in a bigger generic model of ZFC (the one obtained as a generic extension of $L$ via the countable product of the Cohen forcing), and 2nd, via symmetric names. Jech notes in one of his books that both methods yield exactly same models. I wonder is there any consistent proof somewhere as a source of reference?

$\begingroup$ Tip: there is a tag (referencerequest) exactly for the questions like yours. $\endgroup$ – Wojowu Mar 26 '17 at 11:46
You might want to look at Grigorieff's paper which shows that every symmetric model is of the form $\mathrm{HOD}(V\cup X)^{V[G]}$, where $X\in V[G]$.
In the case of Cohen's model, it is easy to argue that $\mathrm{HOD}(A)$ is a submodel of the symmetric extension. From Grigorieff's paper you can extract (although not without difficulty) the needed information to get that this is exactly the symmetric model.
Grigorieff, Serge, Intermediate submodels and generic extensions in set theory, Ann. Math. (2) 101, 447490 (1975). ZBL0308.02060.
(Essentially the idea is that you have a set of generators, and the groups which stabilize them form a basis for the filter of subgroups; then the ordinal is used to "choose a name" and give some sort of "partial interpretation". So in the case of Cohen's model, this would be fixing finitely many reals.)
I can offer another route, though, since we start over $L$ and the Cohen forcing is homogeneous, you might as well consider this as $L(A)$ instead. That would be the HalpernLevy model, which one can show even "more by hand" that it is equivalent to the symmetric extension. Simply because every $x$ in $L(A)$ is definable from some finitely many elements of $A$, and $A$ itself. And that just tells you what is the support and the name in the symmetric extension.
This is [very] implicit in Jech's proof of the fact the model is linearly ordered in his Axiom of Choice book (Ch. 5), and in many papers of Gordon P. Monro, and others from that era (e.g. Felgner's book and more).

$\begingroup$ Well, unfortunately it takes 6 or so pages in Jech, deeply contaminated with the boolean algebra stuff. Minimally I'd like to prove selfcontainedly that the symmetric version of the construction satisfies: all sets belong to HOD($A$). I need a really selfcontained proof since I want to prove that this model $L(A)$, even after extending by another real $x$ (say random or Mathias($U$), to begin with) keeps the Dfiniteness and the existence of a free ultrafilter. It needs an OD($A,x$) wellordering inside, so the same problem arizes in a much more difficult setting. But thank you for the help. $\endgroup$ – Vladimir Kanovei Mar 26 '17 at 15:37

$\begingroup$ Yes, these things are often complicated. I'd be happy to help, feel free to drop me an email with some details if you're interested. $\endgroup$ – Asaf Karagila Mar 26 '17 at 15:41

$\begingroup$ By the way you are right, Cohen's original technique, which is essentially $L(A)$, is perhaps most instrumental for major facts including the ultrafilter existence and all sets being HOD($A$). $\endgroup$ – Vladimir Kanovei Mar 26 '17 at 19:22

$\begingroup$ Well, Cohen's original forcing was based on his definition of forcing, which is now known as "weak forcing" (or is it "strong forcing"? I always forget), and things were a bit weirder there. As far as I know, it was Halpern and Levy who formalized the construction as $L(A)$. $\endgroup$ – Asaf Karagila Mar 26 '17 at 19:53

$\begingroup$ One of key things which I am interested to fix is to prove that every set $x\in\text{HOD}(A)$ is a member of $\text{OD}(A)$ inside $\text{HOD}(A)$. What if we extend $\text{HOD}(A)$ by a generic bijection $f:\omega$ onto $A$ (finite conditions)? This looks like a homogeneous forcing $\endgroup$ – Vladimir Kanovei Mar 26 '17 at 21:36