I am dealing with iterate forcing and I am focusing in those properties which are preserved via iterations. In this regard I would like to see that the forcing $\mathbb{P}=(Fn(\omega,2)^\omega)^M$ which is isomorphic to the $\omega-$iteration of $\dot{\mathbb{Q}}_n=\hat{(Fn(\omega,2)^M)}$ does not preserve $\omega_1$. For this pourpose I am willing to see that for every ground model real $f\in2^\omega$ is coded by $f_G=\bigcup G:\omega\times\omega\rightarrow 2$. More precisely, that for every $n\in\omega$ there exists a $m\in\omega$ such that $f(n)=f_G(n,m)$. Is there some way to take advantage of this fact to find a surjection between $(2^\omega)^M$ and $\omega$ in $M[G]$ and thus conclude that $\omega_1$ is collapsed?
Thank you!!
I assume you mean full product, i.e. conditions are $\Pi_{n\in \omega} Fn(\omega, 2)$. Hence the final generic object is a $\omega \times \omega$ matrix (if you only take finite support, then by $\Delta$-system lemma it is ccc, or better any finite support of ccc forcings is ccc). In the full product case, you can easily code any ground model real using genericity. An example is given here: https://mathoverflow.net/questions/114590/forcing-with-product-vs-box-product by Hamkins.