Generic factorization and ccc preservation for two-step iterations

From $K$ put $G=\{p:\mathrm{\exists }\dot{q}\in R(p,\dot{q})\in K\}$ and $H=\{{\dot{q}}_G:\mathrm{\exists }p\in G(p,\dot{q})\in K\}$. Preimages of ground dense subsets of $P$ are dense in the iteration, so $G$ is generic. If ${\dot{D}}_G$ is dense in ${\dot{Q}}_G$, the forcing theorem produces below each pair a name for a second-coordinate extension in $\dot{D}$; [F1] replaces that local name by a forced-equal name in the set carrier $R$. The resulting pairs are dense, and meeting them proves $H$ generic over $M[G]$.

Conversely, for generics $G,H$ take the filter generated by pairs $(p,\dot{q})$ in the restricted iteration with $p\in G$ and ${\dot{q}}_G\in H$. Every quotient condition has a name occurring in $\dot{Q}$, or a locally forced-equal representative in $R$ by [F1], so the same dense-set translation meets every ground dense subset of $P\ast \dot{Q}$. Recursive evaluation of names first by $G$ and then by $H$ proves $M[K]=M[G][H]$.

Suppose $A=\{(p_{\alpha },{\dot{q}}_{\alpha }):\alpha <{\omega }_1^M\}$ were an antichain and put $\dot{I}=\{(\check{\alpha },p_{\alpha }):\alpha <{\omega }_1^M\}$. We prove syntactically that $1_P$ forces the map $\alpha \mapsto {\dot{q}}_{\alpha }$ from $\dot{I}$ into $\dot{Q}$ to have pairwise incompatible, hence distinct, values. Otherwise some $s$ forces distinct $\alpha ,\beta \in \dot{I}$ and a common $\dot{Q}$-extension of their values. The forcing membership clause lets us strengthen below $p_{\alpha }$ and $p_{\beta }$; the existential clause of [F2] then supplies a further condition $t$ and a name $\dot{r}$ with $t⊩\dot{r}{\le }_{\dot{Q}}{\dot{q}}_{\alpha },{\dot{q}}_{\beta }$. By [F1], replace $\dot{r}$ below $t$ by a forced-equal $\rho \in R$. Then $(t,\rho )$ belongs to the restricted iteration and extends both members of $A$, a contradiction. Thus $1_P⊩\dot{I}$ injects into a $\dot{Q}$-antichain. Since $1_P⊩\dot{Q}$ is ccc, $1_P⊩\dot{I}$ is countable.