We start with a ground model $M$ of $\mathsf{ZFC}$ and consider the product measure space $2^{\mathfrak c^+}$, with the $\sigma$-algebra generated by $\{f\mid f(\alpha)=0\}$ for $\alpha<\mathfrak c^+$ and the product measure which assigns to each of those sets measure $1/2$. We look at the poset $P$ whose conditions are the elements of this $\sigma$ algebra of positive measure, where $p$ is stronger than $q$ iff $p\subset q$ and construct a new model $N=M[G]$ for a $P$-generic filter $G$, in other words $N$ is obtained from $M$ by adding $\mathfrak c^+$-many random reals.
I wish to prove the following result:
If $x$ is a set of integers in $N$, then there is an $M$-random real $y$ in $N$ and a set of integers $z$ in $M$ such that $x$ is arithmetic in $(y,z)$. If $y$ is an $M$-random real and $x$ is a set of integers in $M[y]$, then there is a set of integers $z$ in $M$ such that $x$ is arithmetic in $(y,z)$.
which is the first lemma in Friedman's 1980 paper "A consistent Fubini-Tonelli theorem for nonmeasurable functions" and is supposed to be a "straightforward antichain argument", but I'm not seeing that argument, so I'd appreciate a proof or an hint in the correct direction.
Just in case the definition of "arithmetic in $(y,z)$" that I'm using is the one in Kanamori's book, so that being arithmetic in a set $x$ means being definable in the two sorted structure $$\langle {^\omega}\omega,\omega,\mathrm{ap},+,\times,\mathrm{exp},<,0,1\rangle$$ of second order arithmetic by a formula using no functions quantifiers and $x$ as a parameter.
I do not know my proof is correct in full detail. I hope it is helpful.
I will prove the latter statement first. Take a name $\dot{x}$ which corresponds to $x$. For each $n\in\omega$ take $\mathcal{A}_n$ a maximal antichain contained in the set $$\{p \in (\mathcal{B}^*)^M \mid p\text{ is closed and } p\Vdash \check{n}\in\dot{x}\}.$$ By countable chain condition, $\mathcal{A}_n$ is countable; now let $\mathcal{A}_n = \{A_{d_i^n}^M \mid i<\omega\}$ (where $d_i^n$ is a closed Borel code of $M$.)
We know that $n\in x$ iff there is a closed Borel code $c$ such that $A_c^{M[y]}\ni y$ and $A_c^M\Vdash \check{n}\in\dot{x}$. By maximality of $\mathcal{A}_n$, there is $i<\omega$ such that $A^M_c\cap A^M_{d_i^n}$ is not null. By genericity of $y$, $ A^{M[y]}_{d_i^n}\ni y$. Therefore, $$n\in x \implies \exists i\in\omega : A_{d_i^n}\in \mathcal{A}_n \land A_{d_i^n}^{M[y]} \ni y. $$ We can see that the other direction holds, so we actually have the equivalence.
It remains to claim that the right-hand-side is arithmetic. Since we can regard $\mathcal{A}_n$ is countable set of reals in $M$, we can make it to a single real. Moreover, the formula $A_d^{M[y]}\ni y$ is an arithmetic formula (with parameter $d$ and $y$): for an open Borel code $c$, we can see that $A_c^{M[y]}\ni y$ is arithmetic as we can see $y$ belongs to $A_c^{M[y]}$ by checking first some digits of $y$ with respect to open sets coded by $c$. Hence its negation is also arithmetic, which is equivalent to $x\in A_d^{M[y]}\ni y$ for closed code $d$. By encoding $\langle \mathcal{A}_n\mid n<\omega\rangle$ into a single real, we would get $z$ in the second statement.
For the former statement, it is sufficient to show that if $x\in \mathcal{P}^N(\omega)$ then there is a random real $y$ such that $x\in \mathcal{P}^{M[y]}(\omega)$. By mimicing the proof of Lemma 10.17 (e) of Kanamori, we can see that $x\in M[G\cap \mathcal{B}_I]$, where $\mathcal{B}_I$ is a subalgebra generated by $\{f\mid f(\alpha)=0\}$ for $\alpha\in I \in [\mathfrak{c}^+]^\omega$. Since $\mathcal{B}_I$ is isomorphic to the measure algebra over the Cantor set, $M[G\cap \mathcal{B}_I]=V[y]$ for some random real $y$.
Here is a more detailed description on my latter argument. Fix a name $\dot{x}$ corresponding to $x$ and choose a sequence of antichains $\{\mathcal{A}_n\mid n<\omega\}$, whose members of each are closed and decide $\check{n}\in\dot{x}$.
Observe that $|\bigcup_n\mathcal{A}_n|\le \aleph_0$. Each member of $\bigcup_n\mathcal{A}_n$ is closed, and every closed set over our measure algebra is a finite union of countable intersection of sets of the form $\{f\mid f(\alpha)=0\}$ or $\{f\mid f(\alpha)=1\}$. (Uncountable intersection may occur, but in that case, the measure of the intersection should be 0. This is the reason why we can ignore uncountable intersections.) Hence we can extract $I\in [\mathfrak{c}^+]^\omega$ which needs to generate all members of $\bigcup_n \mathcal{A}_n$.