I am trying to prove that for a finite support iteration $\mathbb{P}_\omega$ such that for every $n\in\omega$ $\mathbb{1}\Vdash_{\mathbb{P}_n} \mathbb{Q}_n\;\text{is not ccc}$ the cardinal $\omega_1$ is collapsed. To see this Kunen proposes the following idea:
For every $n$ suppose $\mathbb{1}\Vdash_{\mathbb{P}_n} \sigma_n\subset\mathbb{Q}_n\;\text{antichain}\;\wedge\; \tau_n:\sigma_n\rightarrow \omega_1\;\text{surjective}$. Given $n$ let us denote by $i_{n\omega}$ the canonical embedding bewteen $\mathbb{P}_n$ and $\mathbb{P}_\omega$. Take $G$ a $\mathbb{P}_\omega$- generic filter over $M$ and $G_n=i^{-1}_{n\omega}(G)$, $H_n=\{\dot{q}_G: \dot{q}\in dom(\dot{\mathbb{Q}}_n)\;\wedge\; \exists p\in\mathbb{P}_n (p\frown\dot{q}\in G_{n+1})\} $ the induced $\mathbb{P}_n$-generic filter over $M$ and the $(\dot{\mathbb{Q}}_n)_{G_n}$-generic filter over $M[G_{n}]$. Then, since for every $n$ we have $\mathbb{1}\Vdash_{\mathbb{P}_n} \sigma_n\subset\mathbb{Q}_n\;\text{antichain}$ that $H_n\cap (\sigma_n)_{G_n}=\{q_n\}$. Now define $f(n)=(\tau_n)_{G_n}(q_n)$ and he states that $f$ is surjective.
Is somebody willing to prove me in detail why that function is from $\omega$ onto $(\omega_1)^M$?
I think this is a case where it helps to consider the finite support product version of the question first.
Suppose I have posets $\mathbb{P}_i$ $(i\in\mathbb{N})$, none of which are c.c.c. We want to show that $\mathbb{P}=\bigoplus \mathbb{P}_i$ collapses $\omega_1$ (a condition in $\mathbb{P}$ is a sequence $(p_i)$ with $p_i\in\mathbb{P}_i$, such that for all but finitely many $i$ we have $p_i=1_i$).
Let $A_i$ be an uncountable maximal antichain in $\mathbb{P}_i$, and let $f_i$ be a surjection from $A_i$ onto $\omega_1$ (which exists since $A_i$ is uncountable). Let $G$ be $\mathbb{P}$-generic, and let $g:\omega\rightarrow\omega_1^V$ be given by $$g(n)=f_n(\sigma)$$ iff there is a $(p_i)\in G$ with $p_i=\sigma$ and $\sigma\in A_i$.
I claim that $g$ is onto. Why? Well, suppose $(p_i)\in\mathbb{P}$ is an arbitrary condition, and let $\alpha<\omega_1^V$. Let $j$ be such that $p_j=1_j$; then let $(q_i)$ be the element of $\mathbb{P}$ where $q_i=p_i$ for $i\not=j$, and $f(q_j)=\alpha$ (why does this exist?). Then $(q_i)\le (p_i)$ and forces $\alpha\in ran(g)$.
Now, do you see how to move this line of reasoning to the finite support iteration version?