Consider the first Cohen model, i.e. let $M$ be a countable transitive model of ZFC + $V=L$, let $\mathbb P$ be the poset consisting of finite partial functions from $\omega\times\omega$ to $2$, let $M[G]$ the generic extension adding a sequence $\{a_n\}_{n\in\omega}$ of generic subsets of $\omega$, and let $M\subset N\subset M[G]$ the symmetric model consisting of the sets $\sigma_G$, where $\sigma\in SM^\mathbb P$ is a hereditarily symmetric name, where $\sigma$ is symmetric if there exists a finite set $x\subset\omega$ such that each permutation $f$ of $\omega$ fixing $x$ induces an automorphism of $\mathbb P$ which induces a map $M^\mathbb P\longrightarrow M^\mathbb P$ that fixes $\sigma$.

Now, the ultrafilter $G$ does not belong to $N$, and so, the map $SM^\mathbb P\longrightarrow N$ given by $\sigma\mapsto \sigma_G$ is not definable in $N$.

However, for each finite $x\subset \omega$, we can consider the set (class in $M$) $SM^\mathbb P_x$ of all $\sigma\in SM^\mathbb P$ fixed by all permutations fixing $x$, as well as $N_x=\{\sigma_G\mid \sigma\in SM^\mathbb P_x\}$.

I guess that the map $SM^\mathbb P_x\longrightarrow N_x$ given by $\sigma\mapsto \sigma_G$ should be definable in $N$ from the set $A=\{a_n\mid n\in\omega\}\in N$, the map $f_x:x\longrightarrow N$ given by $f_x(n)=a_n$ (notice that $f_x\in N$) and maybe other parameters in $M$.

My question is if this is true, and the motivation is that I am trying to simplify the exposition of Halpern and Lévy *"The Boolean Prime Ideal Theorem does not Imply the Axiom of Choice"* by showing that the Cohen model is a model of the theory SP described there, but avoiding the formal languaje used to formulate it. I see that all the axioms have a clear translation in standard terms of forcing but the last one, which asserts more or less what I am trying to prove.

Anyway, do you know if something like this is already done?