Exercise of Iterated Forcing from Kunen's book 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$?
 A: 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?
A: Given $\alpha\in\omega_1^M$ my main purpouse is to see that 
$
D_\alpha=\{p\in\mathbb{P}_\omega: \exists n\in\omega\; (p\upharpoonright n \Vdash_{\mathbb{P}_n} \dot{q}_n\in\sigma_n\;\wedge\; \tau_n(\dot{q}_n)=\alpha)\;\wedge\;p\upharpoonright n+1=p\upharpoonright n\frown \dot{q}_n \}
$
is dense.
Right, given $p\in\mathbb{P}_\omega$ then take the least integer $n_0$ such that $p(n)=\dot{{1}}_{\mathbb{P}_n}$ for every $n\geq n_0$. Now recall that $1_{\mathbb{P}_{n_0}}\Vdash \tau_{n_0}:\sigma_{n_0}\rightarrow \omega_1\;\text{onto}$ so $p\upharpoonright n_0\Vdash \tau_{n_0}:\sigma_{n_0}\rightarrow \omega_1\;\text{onto}$. Thus we can choose in $\mathbb{P}_{n_0}$ a $p'\leq p\upharpoonright n_0$ and $\dot{q}_{n_0}\in dom(\sigma_{n_0})$ such that $p'\Vdash \dot{q}_{n_0}\in \sigma_{n_0}\;\wedge\;  \tau_{n_0}(\dot{q}_{n_0})=\alpha$. Note also that since $1\Vdash \sigma_{n_0}\subset \dot{\mathbb{Q}}_n$ we also have $p'\Vdash \dot{q}_{n_0}\in \dot{\mathbb{Q}}_{n_0}$ so $p'\frown \dot{q}_{n_0}\in \mathbb{P}_{n_0+1}$. Now if we define $r$ such that $r(n)=p(n)$ if $n\neq n_0$ and $r(n_0)=\dot{q}_{n_0}$ it is easy to see that $r\in\mathbb{P}_\omega$ and also that $r\in D_\alpha$ and $r\leq p$. 
Taking into account the result above proved, we are ready to see that our function is surjective. Take $\alpha<\omega_1^M$. Since $D_\alpha$ is dense pick a $p\in G\cap D_\alpha$. By definition there exists $n\in\omega$ such that $p\upharpoonright n \Vdash_{\mathbb{P}_n} \dot{q}_n\in\sigma_n\;\wedge\; \tau_n(\dot{q}_n)=\alpha$ and $p\upharpoonright n+1=p\upharpoonright n\frown \dot{q}_n $. Note that, since $p\in G$, then necessarily $p\upharpoonright n\in G_n$ because $p\leq i_{n\omega}(p\upharpoonright n)$ so $i_{n\omega}(p\upharpoonright n)\in G$ (by condition of filter) and thus, by definition of $G_n$, $p\upharpoonright n\in G_n$. In  the same way it can be seen that $p\upharpoonright n+1\in G_{n+1}$ and thus $(\dot{q}_n)_{G_n}\in H_n$.
In summary, we finally conclude that $(\dot{q}_n)_{G_n}\in (\sigma_n)_{G_n}\cap H_n$ and $(\tau_n)_{G_n}((\dot{q}_n)_{G_n})=\alpha$ or, in other words, $f(n)=(\tau_n)_{G_n}({q}_n)=\alpha$.
