[proofplan] We prove the theorem by transfinite induction on the length of the finite-support iteration. The successor step is the two-step preservation argument: if $P$ is ccc and $P$ forces $\dot Q$ to be ccc, then $P * \dot Q$ is ccc. At a limit stage, an uncountable family of finite-support conditions is thinned by the delta-system argument so that their supports have a common finite root; compatibility is then found below the root using the induction hypothesis and extended to the remaining, disjoint coordinates by a finite coordinate-by-coordinate amalgamation. [/proofplan]

[step:Fix the order convention and the induction statement] We use the forcing convention that $q \le p$ means that $q$ is stronger than $p$. Let $\omega_1$ denote the first uncountable ordinal, equivalently the least ordinal of uncountable cardinality. For each $\beta \le \lambda$, a condition $p \in P_\beta$ is a finite-support function with domain contained in $\beta$, where the support of $p$ is the finite set \begin{align*} \operatorname{supp}(p) = \{\alpha < \beta : p(\alpha) \text{ is not the top condition of } \dot Q_\alpha\}. \end{align*} For each $\alpha < \beta$ the value $p(\alpha)$ is a $P_\alpha$-name and \begin{align*} p|_\alpha \Vdash_{P_\alpha} \text{``}p(\alpha) \in \dot Q_\alpha\text{''} \end{align*} whenever $\alpha \in \operatorname{supp}(p)$. Coordinates outside $\operatorname{supp}(p)$ are understood as the top condition of the corresponding iterand. We prove by transfinite induction on $\beta \le \lambda$ that $P_\beta$ is ccc. [/step]

[step:Handle successor stages by the two-step ccc preservation argument] Let $\beta = \alpha + 1$. By the induction hypothesis, $P_\alpha$ is ccc, and by hypothesis, \begin{align*} P_\alpha \Vdash \text{``}\dot Q_\alpha \text{ is ccc.''} \end{align*} We prove that $P_{\alpha+1} = P_\alpha * \dot Q_\alpha$ is ccc. [claim:Two-step iterations preserve ccc] If $P$ is ccc and $P \Vdash \text{``}\dot Q \text{ is ccc''}$, then $P * \dot Q$ is ccc. [/claim] [proof] Suppose toward a contradiction that $A = \{(p_\xi,\dot q_\xi) : \xi < \omega_1\}$ is an antichain in $P * \dot Q$. Let $\dot G$ denote the canonical $P$-name for the generic filter, and define the $P$-name \begin{align*} \dot I = \{\xi < \omega_1 : p_\xi \in \dot G\}. \end{align*} We first verify the preservation fact needed here: ccc forcing cannot make the ground-model ordinal $\omega_1$ countable. More precisely, if $u \in P$ forced that a $P$-name $\dot C$ is a countable subset of $\omega_1$, then $u$ also forces $\dot C \subset C$ for some countable ground-model set $C \subset \omega_1$. To prove this, take a $P$-name $\dot f$ such that \begin{align*} u \Vdash_P \text{``}\dot f: \omega \to \dot C \text{ is surjective.''} \end{align*} For each $n \in \omega$, choose a maximal antichain $B_n \subset P$ below $u$ deciding the value of $\dot f(n)$. Since $P$ is ccc, each $B_n$ is countable. Let $C$ be the set of all ordinals decided as a value of some $\dot f(n)$ by some condition in some $B_n$. Then $C$ is a [countable union of countable sets](/theorems/755), hence countable, and maximality of each $B_n$ gives \begin{align*} u \Vdash_P \text{``}\operatorname{range}(\dot f) \subset C\text{.''} \end{align*} Thus $u \Vdash_P \text{``}\dot C \subset C\text{''}$. We now show that there is some $p_* \in P$ such that \begin{align*} p_* \Vdash_P \text{``}\dot I \text{ is uncountable.''} \end{align*} If no such $p_*$ existed, then the top condition would force $\dot I$ to be countable. By the preservation argument just proved, $\dot I$ would be covered by a countable ground-model subset of $\omega_1$. But $p_\xi \Vdash_P \xi \in \dot I$ for every $\xi < \omega_1$, contradicting the existence of such a countable cover. Now work below $p_*$. Since $p_* \Vdash_P \text{``}\dot I \text{ is uncountable''}$ and $P \Vdash_P \text{``}\dot Q \text{ is ccc''}$, no extension of $p_*$ can force that $\{\dot q_\xi : \xi \in \dot I\}$ is an antichain in $\dot Q$. Therefore there is an extension $p_0 \le p_*$ forcing that two distinct members of this family are compatible in $\dot Q$. Strengthening $p_0$ if necessary, choose ground-model ordinals $\xi,\eta < \omega_1$ with $\xi \ne \eta$ such that \begin{align*} p_0 \Vdash_P \text{``}\xi \in \dot I \text{ and } \eta \in \dot I \text{ and } \dot q_\xi \text{ is compatible with } \dot q_\eta \text{ in } \dot Q\text{.''} \end{align*} The assertions $\xi \in \dot I$ and $\eta \in \dot I$ mean exactly that $p_\xi \in \dot G$ and $p_\eta \in \dot G$. Thus $p_0$ is compatible in $P$ with both $p_\xi$ and $p_\eta$; by strengthening once more, take $p \le p_0,p_\xi,p_\eta$ in $P$. Finally, strengthen $p$ to decide a common lower bound in $\dot Q$: there is a $P$-name $\dot r$ such that \begin{align*} p \Vdash_P \text{``}\dot r \le_{\dot Q} \dot q_\xi \text{ and } \dot r \le_{\dot Q} \dot q_\eta\text{.''} \end{align*} Then $(p,\dot r)$ is a condition in $P * \dot Q$ extending both $(p_\xi,\dot q_\xi)$ and $(p_\eta,\dot q_\eta)$, contradicting that $A$ is an antichain. Thus $P * \dot Q$ is ccc. [/proof] Applying the claim with $P = P_\alpha$ and $\dot Q = \dot Q_\alpha$ gives that $P_{\alpha+1}$ is ccc. [/step]

[step:Thin an uncountable family of finite supports at a limit stage]Let $\beta \le \lambda$ be a limit ordinal, and assume $P_\gamma$ is ccc for every $\gamma < \beta$. Suppose toward a contradiction that $A \subseteq P_\beta$ is an uncountable antichain. Choose an uncountable subfamily indexed as $A_0 = \{p_\xi : \xi < \omega_1\} \subseteq A$. For each $\xi < \omega_1$, define the finite support \begin{align*} F_\xi = \operatorname{supp}(p_\xi) \subset \beta. \end{align*} By the finite delta-system argument proved in the guided expansion below, after passing to an uncountable subset of $\omega_1$, there is a finite set $R \subset \beta$ such that \begin{align*} F_\xi \cap F_\eta = R \end{align*} for all distinct remaining indices $\xi,\eta$.[/step]

[guided]We now isolate the common part of the supports. For each condition $p_\xi$, its support $F_\xi = \operatorname{supp}(p_\xi)$ is finite by the definition of finite-support iteration, where $\operatorname{supp}(p_\xi)$ denotes the set of coordinates at which $p_\xi$ is not the top condition. The delta-system lemma says that an uncountable family of finite sets contains an uncountable delta-system: after thinning the index set, there is one finite set $R$ such that any two distinct supports meet exactly in $R$. Here is the standard verification. For each $n \in \omega$, let $I_n = \{\xi < \omega_1 : |F_\xi| = n\}$. The sets $I_n$ partition $\omega_1$ into countably many pieces, so at least one $I_n$ is uncountable; otherwise $\omega_1$ would be a countable union of countable sets. Restricting to that uncountable $I_n$, all supports have the same finite size $n$. We argue by induction on $n$. The case $n = 0$ is immediate. If some ordinal $\rho$ belongs to uncountably many supports, remove $\rho$ from those supports and apply the induction hypothesis to the resulting sets of size $n-1$; adjoining $\rho$ to the resulting root gives the desired root. If no ordinal belongs to uncountably many supports, construct recursively an $\omega_1$-sequence of supports that are pairwise disjoint: at each countable stage, only countably many ordinals have appeared so far, and each belongs to only countably many supports, so only countably many supports are forbidden. This gives a delta-system with empty root. Thus in all cases we obtain an uncountable subfamily with common finite root $R$. After replacing $A_0$ by this uncountable subfamily, the exact conclusion needed for the limit-stage argument is that \begin{align*} \operatorname{supp}(p_\xi) \cap \operatorname{supp}(p_\eta) = R \end{align*} whenever $\xi \ne \eta$. Thus the common coordinates are precisely the finite root $R$, and all non-root coordinates of two distinct remaining conditions are disjoint.[/guided]

[step:Find two conditions whose common-root initial parts are compatible] If $R = \varnothing$, set $\gamma = 0$. If $R \ne \varnothing$, define \begin{align*} \gamma = \sup R + 1. \end{align*} Since $R$ is finite and $R \subset \beta$, we have $\gamma < \beta$. For every remaining index $\xi$, the restriction $p_\xi|_\gamma$ is a condition in $P_\gamma$. By the induction hypothesis, $P_\gamma$ is ccc. Therefore the uncountable family \begin{align*} \{p_\xi|_\gamma : \xi < \omega_1\} \end{align*} cannot be an antichain in $P_\gamma$. Hence there are distinct indices $\xi,\eta < \omega_1$ and a condition $r \in P_\gamma$ such that \begin{align*} r \le p_\xi|_\gamma \end{align*} and \begin{align*} r \le p_\eta|_\gamma. \end{align*} Set $p = p_\xi$ and $q = p_\eta$. [/step]

[step:Amalgamate the two conditions above the common initial segment] We construct a condition $s \in P_\beta$ extending both $p$ and $q$, and we verify the forcing-iteration compatibility point coordinate by coordinate. Let \begin{align*} D = \bigl(\operatorname{supp}(p) \cup \operatorname{supp}(q)\bigr) \setminus \gamma. \end{align*} The set $D$ is finite. Since the supports form a delta-system with root $R \subset \gamma$, no coordinate in $D$ belongs to both $\operatorname{supp}(p)$ and $\operatorname{supp}(q)$. List $D$ in increasing order as $\delta_1 < \cdots < \delta_m$. Define a finite-support function $s$ as follows. Below $\gamma$, set $s|_\gamma = r$. If $\delta_j \in \operatorname{supp}(p) \setminus \operatorname{supp}(q)$, set \begin{align*} s(\delta_j) = p(\delta_j). \end{align*} If $\delta_j \in \operatorname{supp}(q) \setminus \operatorname{supp}(p)$, set \begin{align*} s(\delta_j) = q(\delta_j). \end{align*} At all coordinates not in $\operatorname{supp}(r) \cup D$, assign the top condition of the corresponding iterand. Thus \begin{align*} \operatorname{supp}(s) \subset \operatorname{supp}(r) \cup D, \end{align*} so $s$ has finite support. We prove by induction on $j \in \{0,1,\dots,m\}$ that $s|_{\theta_j}$ is a condition extending both $p|_{\theta_j}$ and $q|_{\theta_j}$, where $\theta_0 = \gamma$ and $\theta_j = \delta_j + 1$ for $j \ge 1$. The case $j=0$ holds because $s|_\gamma = r$ and $r \le p|_\gamma,q|_\gamma$. Assume the assertion holds through the initial segment below $\delta_j$. If $\delta_j \in \operatorname{supp}(p) \setminus \operatorname{supp}(q)$, then the induction hypothesis gives $s|_{\delta_j} \le p|_{\delta_j}$. Since $p$ is a condition, \begin{align*} p|_{\delta_j} \Vdash_{P_{\delta_j}} \text{``}p(\delta_j) \in \dot Q_{\delta_j}\text{.''} \end{align*} By monotonicity of forcing, $s|_{\delta_j}$ forces the same statement. Also $q(\delta_j)$ is the top condition because $\delta_j \notin \operatorname{supp}(q)$, so $s|_{\delta_j}$ forces \begin{align*} p(\delta_j) \le_{\dot Q_{\delta_j}} q(\delta_j). \end{align*} Since $s(\delta_j)=p(\delta_j)$, this shows that $s|_{\delta_j+1}$ is a condition extending both $p|_{\delta_j+1}$ and $q|_{\delta_j+1}$. The case $\delta_j \in \operatorname{supp}(q) \setminus \operatorname{supp}(p)$ is the same argument with $p$ and $q$ interchanged: the induction hypothesis gives $s|_{\delta_j} \le q|_{\delta_j}$, the fact that $q$ is a condition makes $q(\delta_j)$ a forced member of $\dot Q_{\delta_j}$, and $p(\delta_j)$ is top. This induction also explains why earlier copied coordinates from the other condition cause no difficulty: at a coordinate where one condition is nontrivial and the other has top, the copied nontrivial name is forced below the top coordinate of the other condition. Therefore the induction maintains extension of both initial segments, not merely legality over the condition from which the current coordinate was copied. After $m$ steps, $s$ is a legitimate condition in $P_\beta$. The same induction proves that $s|_{\theta_m}$ extends both $p|_{\theta_m}$ and $q|_{\theta_m}$. Above the last coordinate in $D$, both $p$ and $q$ have only top coordinates, while $s$ also has only top coordinates. Hence \begin{align*} s \le p \end{align*} and \begin{align*} s \le q. \end{align*} [/step]

[step:Contradict the antichain assumption and close the induction] The conditions $p$ and $q$ were distinct members of the assumed antichain $A$, but the condition $s \in P_\beta$ extends both of them. This contradicts the definition of an antichain. Therefore no uncountable antichain exists in $P_\beta$, so $P_\beta$ is ccc. The successor and limit cases complete the transfinite induction. Taking $\beta = \lambda$, we conclude that $P_\lambda$ is ccc. [/step]