[proofplan] We prove the theorem by transfinite induction on the length of the finite-support iteration. Successor stages are handled by the internal two-step preservation claim: a ccc forcing followed by a forced-ccc forcing is ccc. At limit stages, an uncountable family of finite-support conditions is thinned by the Delta-system lemma so that the supports have a common finite root; the induction hypothesis gives compatibility below the root, and finite support lets us merge two conditions outside the root because their remaining supports are disjoint. [/proofplan]

[step:Prove the two-step preservation lemma for ccc forcing][claim:Two-step ccc preservation] Let $P$ be a ccc forcing notion, and let $\dot{Q}$ be a $P$-name such that \begin{align*} 1_P\Vdash_P ``\dot{Q}\text{ is ccc}''. \end{align*} Then the two-step iteration $P*\dot{Q}$ is ccc. [/claim] [proof] Let $\omega_1$ denote the first uncountable ordinal. Suppose, toward a contradiction, that \begin{align*} A=\{(p_\xi,\dot{q}_\xi):\xi<\omega_1\} \end{align*} is an uncountable antichain in $P*\dot{Q}$. Here each $p_\xi\in P$ and each $\dot{q}_\xi$ is a $P$-name such that \begin{align*} p_\xi\Vdash_P ``\dot{q}_\xi\in \dot{Q}''. \end{align*} We first use the following standard ccc capture fact. If $P$ is ccc and $\{p_\xi:\xi<\omega_1\}\subset P$, then there is a condition $p_*\in P$ such that \begin{align*} p_*\Vdash_P ``\{\xi<\omega_1:p_\xi\in \dot{G}\}\text{ is uncountable}''. \end{align*} We prove the capture fact, using the standard ccc preservation fact that ccc forcing preserves $\omega_1$ and, equivalently here, whenever a condition forces a subset of the ground-model ordinal $\omega_1$ to be countable, some stronger condition forces that subset to be bounded below a ground-model countable ordinal. This preservation fact applies because $P$ is ccc. Indeed, if no such $p_*$ existed, then for every $p\in P$, the condition $p$ would fail to force that $\{\xi<\omega_1:p_\xi\in\dot G\}$ is uncountable. Hence some $p'\leq_P p$ would force this set to be countable. By the ccc preservation and bounding fact just stated, there would be some $r\leq_P p'$ and some $\delta<\omega_1$ such that \begin{align*} r\Vdash_P ``\{\xi<\omega_1:p_\xi\in\dot G\}\subset\delta''. \end{align*} Equivalently, $r$ is incompatible with every $p_\xi$ for $\xi\geq\delta$: if $r$ had a common strengthening with such a $p_\xi$, that strengthening would force $p_\xi\in\dot G$, contradicting the displayed statement. Let $M\subset P$ be a maximal antichain of conditions $r$ for which such a countable ordinal $\delta_r<\omega_1$ exists. Since $P$ is ccc, $M$ is countable. For each $r\in M$, choose $\delta_r<\omega_1$ such that $r$ is incompatible with every $p_\xi$ for $\xi\geq\delta_r$, and define \begin{align*} \delta_*=\sup\{\delta_r:r\in M\}<\omega_1. \end{align*} For any $\xi\geq\delta_*$, the condition $p_\xi$ is incompatible with every $r\in M$, contradicting the maximality of $M$. This proves the capture fact. Apply the capture fact to $\{p_\xi:\xi<\omega_1\}$. Let $\dot{G}$ denote the canonical $P$-name for the $P$-generic filter. Choose $p_*\in P$ such that \begin{align*} p_*\Vdash_P ``I=\{\xi<\omega_1:p_\xi\in \dot{G}\}\text{ is uncountable}''. \end{align*} In any $P$-generic extension containing $p_*$, consider the indexed family \begin{align*} (\dot{q}_\xi^{\dot{G}})_{\xi\in I}. \end{align*} We show that its distinct-index members are pairwise incompatible in $\dot{Q}^{\dot{G}}$. Since a condition is compatible with itself, pairwise incompatibility for distinct indices implies that the values are distinct; hence the set \begin{align*} B=\{\dot{q}_\xi^{\dot{G}}:\xi\in I\} \end{align*} is uncountable and is an antichain in $\dot{Q}^{\dot{G}}$. To prove pairwise incompatibility, take distinct $\xi,\eta\in I$. Then $p_\xi$ and $p_\eta$ both belong to the generic filter, so they have a common strengthening in the generic filter. If $\dot{q}_\xi^{\dot{G}}$ and $\dot{q}_\eta^{\dot{G}}$ were compatible in $\dot{Q}^{\dot{G}}$, the [forcing theorem](/theorems/6531) would give a condition $r\leq_P p_\xi,p_\eta$ and a $P$-name $\dot{s}$ such that \begin{align*} r\Vdash_P ``\dot{s}\leq_{\dot{Q}}\dot{q}_\xi\text{ and }\dot{s}\leq_{\dot{Q}}\dot{q}_\eta''. \end{align*} Then $(r,\dot{s})$ would be a common strengthening of $(p_\xi,\dot{q}_\xi)$ and $(p_\eta,\dot{q}_\eta)$ in $P*\dot{Q}$, contradicting that $A$ is an antichain. Thus $p_*$ forces that $\dot{Q}$ contains an uncountable antichain, contradicting \begin{align*} 1_P\Vdash_P ``\dot{Q}\text{ is ccc}''. \end{align*} Therefore $P*\dot{Q}$ is ccc. [/proof][/step]

[guided]Let $\omega_1$ denote the first uncountable ordinal. Suppose, toward a contradiction, that \begin{align*} A=\{(p_\xi,\dot{q}_\xi):\xi<\omega_1\} \end{align*} is an uncountable antichain in $P*\dot{Q}$. For each $\xi<\omega_1$, the first coordinate satisfies $p_\xi\in P$, and the second coordinate is a $P$-name satisfying \begin{align*} p_\xi\Vdash_P ``\dot{q}_\xi\in \dot{Q}''. \end{align*} We need a way to see uncountably many first coordinates inside one generic extension. The ccc capture fact says: if $P$ is ccc and $\{p_\xi:\xi<\omega_1\}\subset P$, then some condition $p_*\in P$ forces uncountably many of the $p_\xi$ to belong to the generic filter. We prove this fact because it is the mechanism that transfers the antichain from $P*\dot{Q}$ to $\dot{Q}$. Assume the capture fact fails. We need one standard preservation input here: ccc forcing preserves $\omega_1$, and consequently if a condition forces a subset of the ground-model ordinal $\omega_1$ to be countable, then a stronger condition forces that subset to be bounded by some ground-model countable ordinal. This input applies because $P$ is ccc. Now fix any $p\in P$. Since the capture fact is assumed to fail, $p$ does not force the set $\{\xi<\omega_1:p_\xi\in\dot G\}$ to be uncountable. Hence there is a stronger condition $p'\leq_P p$ forcing that this set is countable. Applying the ccc preservation and bounding fact to $p'$, we obtain a condition $r\leq_P p'$ and an ordinal $\delta<\omega_1$ such that \begin{align*} r\Vdash_P ``\{\xi<\omega_1:p_\xi\in\dot G\}\subset\delta''. \end{align*} This is equivalent to saying that $r$ is incompatible with every $p_\xi$ for $\xi\geq\delta$: if $r$ were compatible with such a $p_\xi$, then a common strengthening of $r$ and $p_\xi$ would force $p_\xi$ to be in the generic filter, contradicting the displayed boundedness statement. Let $M\subset P$ be a maximal antichain of conditions with this tail-incompatibility property. Since $P$ is ccc, $M$ is countable. For each $r\in M$, choose an ordinal $\delta_r<\omega_1$ such that $r$ is incompatible with every $p_\xi$ for $\xi\geq\delta_r$, and define \begin{align*} \delta_*=\sup\{\delta_r:r\in M\}. \end{align*} Because $M$ is countable and every $\delta_r$ is countable, $\delta_*<\omega_1$. If $\xi\geq\delta_*$, then $p_\xi$ is incompatible with every $r\in M$. This contradicts the maximality of $M$, since maximality requires every condition in $P$ to be compatible with some member of $M$. Hence the capture fact holds. Let $\dot{G}$ denote the canonical $P$-name for the $P$-generic filter. Applying the capture fact to $\{p_\xi:\xi<\omega_1\}$ gives $p_*\in P$ such that \begin{align*} p_*\Vdash_P ``I=\{\xi<\omega_1:p_\xi\in \dot{G}\}\text{ is uncountable}''. \end{align*} In any $P$-generic extension containing $p_*$, first consider the indexed family \begin{align*} (\dot{q}_\xi^{\dot{G}})_{\xi\in I}. \end{align*} We show that $p_*$ forces distinct-index members of this family to be pairwise incompatible in $\dot{Q}$. This is enough to get an uncountable antichain: if two indices gave the same value, that value would be compatible with itself, so pairwise incompatibility for distinct indices also proves the values are distinct. Thus \begin{align*} B=\{\dot{q}_\xi^{\dot{G}}:\xi\in I\} \end{align*} is forced to be an uncountable antichain in $\dot{Q}$. Take distinct $\xi,\eta\in I$. Since $p_\xi$ and $p_\eta$ both belong to the same generic filter, they have a common strengthening in that filter. If $\dot{q}_\xi^{\dot{G}}$ and $\dot{q}_\eta^{\dot{G}}$ were compatible in $\dot{Q}^{\dot{G}}$, then the forcing theorem gives a condition $r\in P$ below both first coordinates and a $P$-name $\dot{s}$ such that \begin{align*} r\leq_P p_\xi \end{align*} and \begin{align*} r\leq_P p_\eta \end{align*} and \begin{align*} r\Vdash_P ``\dot{s}\leq_{\dot{Q}}\dot{q}_\xi\text{ and }\dot{s}\leq_{\dot{Q}}\dot{q}_\eta''. \end{align*} Then $(r,\dot{s})$ is a common strengthening of $(p_\xi,\dot{q}_\xi)$ and $(p_\eta,\dot{q}_\eta)$ in $P*\dot{Q}$. This contradicts that $A$ is an antichain. Therefore $p_*$ forces that $\dot{Q}$ contains an uncountable antichain. This contradicts \begin{align*} 1_P\Vdash_P ``\dot{Q}\text{ is ccc}''. \end{align*} So no uncountable antichain exists in $P*\dot{Q}$, and the two-step iteration is ccc.[/guided]

[step:Run the induction through successor stages] We prove by transfinite induction on $\lambda\leq\kappa$ that $P_\lambda$ is ccc. The base case is $\lambda=0$. The forcing $P_0$ has only its top condition, so every antichain in $P_0$ has at most one element. Now suppose $\lambda=\alpha+1$ and $P_\alpha$ is ccc. By the hypothesis of the theorem, \begin{align*} 1_{P_\alpha}\Vdash_{P_\alpha} ``\dot{Q}_\alpha\text{ is ccc}''. \end{align*} The successor stage of the finite-support iteration is \begin{align*} P_{\alpha+1}=P_\alpha*\dot{Q}_\alpha. \end{align*} By the two-step ccc preservation claim, $P_{\alpha+1}$ is ccc. [/step]

[step:Thin an uncountable antichain at a limit stage to a Delta-system of supports] Let $\lambda\leq\kappa$ be a limit ordinal, and assume inductively that $P_\alpha$ is ccc for every $\alpha<\lambda$. Suppose, toward a contradiction, that $A\subset P_\lambda$ is an uncountable antichain. Choose a subfamily \begin{align*} \{p_\xi:\xi<\omega_1\}\subset A \end{align*} of pairwise distinct conditions. For each $\xi<\omega_1$, define the finite support of $p_\xi$ by \begin{align*} \operatorname{supp}(p_\xi)=\{\alpha<\lambda:p_\xi\restriction\alpha\text{ does not force }p_\xi(\alpha)\text{ to be the top condition of }\dot{Q}_\alpha\}. \end{align*} We use the standard finite-support convention that each condition is represented with the canonical top name at every coordinate outside its finite domain; with this convention, coordinates outside $\operatorname{supp}(p_\xi)$ are forced by the earlier restriction to be top coordinates. Since the iteration has finite support, $\{\operatorname{supp}(p_\xi):\xi<\omega_1\}$ is an uncountable family of finite sets. Applying the Delta-system lemma to this uncountable family of finite sets, there are an uncountable set $I\subset\omega_1$ and a finite set $u\subset\lambda$ such that \begin{align*} \operatorname{supp}(p_\xi)\cap\operatorname{supp}(p_\eta)=u \end{align*} for all distinct $\xi,\eta\in I$. If $u=\varnothing$, set $\beta=0$. If $u\neq\varnothing$, set \begin{align*} \beta=\sup(u)+1. \end{align*} Because $u$ is finite and $\lambda$ is a limit ordinal, we have $\beta<\lambda$. [/step]

[step:Find two conditions with compatible restrictions below the root] For each $\xi\in I$, let $p_\xi\restriction\beta\in P_\beta$ denote the restriction of $p_\xi$ to coordinates below $\beta$. By the induction hypothesis, $P_\beta$ is ccc. Hence the uncountable family \begin{align*} \{p_\xi\restriction\beta:\xi\in I\} \end{align*} cannot be an antichain in $P_\beta$. Choose distinct $\xi,\eta\in I$ and a condition $r\in P_\beta$ such that \begin{align*} r\leq_{P_\beta}p_\xi\restriction\beta \end{align*} and \begin{align*} r\leq_{P_\beta}p_\eta\restriction\beta. \end{align*} [/step]

[step:Merge the two conditions using disjointness outside the root]We define a finite-support condition $s\in P_\lambda$ as follows. Below $\beta$, set \begin{align*} s\restriction\beta=r. \end{align*} For each $\alpha\in\operatorname{supp}(p_\xi)\setminus\beta$, set \begin{align*} s(\alpha)=p_\xi(\alpha). \end{align*} For each $\alpha\in\operatorname{supp}(p_\eta)\setminus\beta$, set \begin{align*} s(\alpha)=p_\eta(\alpha). \end{align*} At every remaining coordinate $\alpha<\lambda$, set $s(\alpha)$ to be the canonical top name for $\dot{Q}_\alpha$. The definition is consistent because \begin{align*} (\operatorname{supp}(p_\xi)\setminus u)\cap(\operatorname{supp}(p_\eta)\setminus u)=\varnothing \end{align*} and every element of $u$ lies below $\beta$. The support of $s$ is contained in the finite set \begin{align*} \operatorname{supp}(r)\cup\operatorname{supp}(p_\xi)\cup\operatorname{supp}(p_\eta), \end{align*} so $s$ has finite support. We verify simultaneously by induction on $\alpha\leq\lambda$ that $s\restriction\alpha\in P_\alpha$, that $s\restriction\alpha\leq_{P_\alpha}p_\xi\restriction\alpha$, and that $s\restriction\alpha\leq_{P_\alpha}p_\eta\restriction\alpha$, where $\leq_{P_\alpha}$ denotes the forcing order on $P_\alpha$. We use two order facts at successor coordinates. First, monotonicity of forcing says that if $a\leq_{P_\alpha}b$ and $b\Vdash_{P_\alpha}\varphi$, then $a\Vdash_{P_\alpha}\varphi$. Second, by the top-name convention, if $\alpha\notin\operatorname{supp}(p)$, then $p\restriction\alpha$ forces that $p(\alpha)$ is the top condition of $\dot Q_\alpha$, so every forced condition in $\dot Q_\alpha$ is below it. For $\alpha\leq\beta$, the induction assertion follows from $s\restriction\beta=r$ and the fact that $r$ is a common strengthening of $p_\xi\restriction\beta$ and $p_\eta\restriction\beta$. Let $\alpha$ satisfy $\beta\leq\alpha<\lambda$, and assume the induction statement holds at stage $\alpha$. If $\alpha\in\operatorname{supp}(p_\xi)\setminus\beta$, then $\alpha\notin\operatorname{supp}(p_\eta)$, because all common support coordinates lie in $u\subset\beta$. Hence $p_\eta\restriction\alpha$ forces that $p_\eta(\alpha)$ is the top condition of $\dot{Q}_\alpha$. Since $s\restriction\alpha\leq_{P_\alpha}p_\xi\restriction\alpha$, monotonicity of forcing gives that $s\restriction\alpha$ forces $s(\alpha)=p_\xi(\alpha)$ to be an element of $\dot Q_\alpha$ and to satisfy $s(\alpha)\leq_{\dot Q_\alpha}p_\xi(\alpha)$. Since $s\restriction\alpha\leq_{P_\alpha}p_\eta\restriction\alpha$, the top-name convention gives that $s\restriction\alpha$ also forces $p_\eta(\alpha)$ to be the top condition of $\dot Q_\alpha$; hence it forces $s(\alpha)\leq_{\dot Q_\alpha}p_\eta(\alpha)$. Therefore the extension requirement at coordinate $\alpha$ holds for both $p_\xi$ and $p_\eta$. If $\alpha\in\operatorname{supp}(p_\eta)\setminus\beta$, then $\alpha\notin\operatorname{supp}(p_\xi)$, because all common support coordinates lie in $u\subset\beta$. Hence $p_\xi\restriction\alpha$ forces that $p_\xi(\alpha)$ is the top condition of $\dot{Q}_\alpha$. Since $s\restriction\alpha\leq_{P_\alpha}p_\eta\restriction\alpha$, monotonicity of forcing gives that $s\restriction\alpha$ forces $s(\alpha)=p_\eta(\alpha)$ to be an element of $\dot Q_\alpha$ and to satisfy $s(\alpha)\leq_{\dot Q_\alpha}p_\eta(\alpha)$. Since $s\restriction\alpha\leq_{P_\alpha}p_\xi\restriction\alpha$, the top-name convention gives that $s\restriction\alpha$ also forces $p_\xi(\alpha)$ to be the top condition of $\dot Q_\alpha$; hence it forces $s(\alpha)\leq_{\dot Q_\alpha}p_\xi(\alpha)$. Therefore the extension requirement at coordinate $\alpha$ holds for both $p_\xi$ and $p_\eta$. If $\alpha$ belongs to neither support, then both $p_\xi\restriction\alpha$ and $p_\eta\restriction\alpha$ force their coordinate values to be top conditions in $\dot{Q}_\alpha$, and $s(\alpha)$ is defined to be the canonical top name, so the extension requirement again holds. Limit stages of this coordinate induction follow from finite-support restriction. Consequently \begin{align*} s\leq_{P_\lambda}p_\xi \end{align*} and \begin{align*} s\leq_{P_\lambda}p_\eta. \end{align*}[/step]

[guided]The purpose of the Delta-system thinning was to make the two tails compatible by construction. The only possible conflicts between $p_\xi$ and $p_\eta$ occur on coordinates that both supports mention. After thinning, the common part of the supports is the finite root $u$, and we chose $\beta$ above that root. Compatibility below $\beta$ is handled by the condition $r\in P_\beta$. We now build one condition $s\in P_\lambda$ that keeps this common strengthening below $\beta$ and then copies the two original conditions on their separate tails. Formally, define \begin{align*} s\restriction\beta=r. \end{align*} If $\alpha\in\operatorname{supp}(p_\xi)\setminus\beta$, define \begin{align*} s(\alpha)=p_\xi(\alpha). \end{align*} If $\alpha\in\operatorname{supp}(p_\eta)\setminus\beta$, define \begin{align*} s(\alpha)=p_\eta(\alpha). \end{align*} At all other coordinates, define $s(\alpha)$ to be the canonical top name for $\dot{Q}_\alpha$. Why is this well-defined? The supports of $p_\xi$ and $p_\eta$ meet exactly in $u$, and $u\subset\beta$. Therefore no coordinate at or above $\beta$ belongs to both supports. So the two copying rules never assign two different values to the same coordinate. Why is $s$ a finite-support condition? Its nontrivial coordinates are contained in \begin{align*} \operatorname{supp}(r)\cup\operatorname{supp}(p_\xi)\cup\operatorname{supp}(p_\eta). \end{align*} Each of these three supports is finite, so their union is finite. Finally, we check the forcing-order requirement by a simultaneous coordinate induction. The induction assertion at a stage $\alpha\leq\lambda$ is that $s\restriction\alpha$ is a condition in $P_\alpha$ and extends both $p_\xi\restriction\alpha$ and $p_\eta\restriction\alpha$. The coordinate values $p_\xi(\alpha)$ and $p_\eta(\alpha)$ are $P_\alpha$-names. We use two facts repeatedly: monotonicity of forcing preserves forced membership and order statements under stronger earlier restrictions, and the finite-support top-name convention says that outside the support of a condition, the earlier restriction forces the coordinate value to be the top condition of the next forcing. For every $\alpha\leq\beta$, this is exactly what $r\leq_{P_\beta}p_\xi\restriction\beta,p_\eta\restriction\beta$ gives. Now suppose $\beta\leq\alpha<\lambda$ and the assertion has been proved at $\alpha$. If $\alpha\in\operatorname{supp}(p_\xi)\setminus\beta$, then disjointness of the Delta-system tails gives $\alpha\notin\operatorname{supp}(p_\eta)$. Thus $p_\eta\restriction\alpha$ forces that $p_\eta(\alpha)$ is the top condition of $\dot{Q}_\alpha$. The induction hypothesis gives $s\restriction\alpha\leq_{P_\alpha}p_\xi\restriction\alpha$ and $s\restriction\alpha\leq_{P_\alpha}p_\eta\restriction\alpha$. By monotonicity, $s\restriction\alpha$ forces that $s(\alpha)=p_\xi(\alpha)$ is an element of $\dot Q_\alpha$ and is below $p_\xi(\alpha)$. By the top-name convention applied to $p_\eta$, the same earlier restriction also forces that $p_\eta(\alpha)$ is the top condition of $\dot Q_\alpha$, so it forces $s(\alpha)\leq_{\dot Q_\alpha}p_\eta(\alpha)$. So adding this coordinate preserves extension of both original conditions. If $\alpha\in\operatorname{supp}(p_\eta)\setminus\beta$, then the Delta-system tail disjointness gives $\alpha\notin\operatorname{supp}(p_\xi)$. Thus $p_\xi\restriction\alpha$ forces that $p_\xi(\alpha)$ is the top condition of $\dot{Q}_\alpha$. The induction hypothesis gives $s\restriction\alpha\leq_{P_\alpha}p_\eta\restriction\alpha$ and $s\restriction\alpha\leq_{P_\alpha}p_\xi\restriction\alpha$. By monotonicity, $s\restriction\alpha$ forces that $s(\alpha)=p_\eta(\alpha)$ is an element of $\dot Q_\alpha$ and is below $p_\eta(\alpha)$. By the top-name convention applied to $p_\xi$, the same earlier restriction also forces that $p_\xi(\alpha)$ is the top condition of $\dot Q_\alpha$, so it forces $s(\alpha)\leq_{\dot Q_\alpha}p_\xi(\alpha)$. So adding this coordinate preserves extension of both original conditions. If $\alpha$ is in neither support, then all three conditions use top names at coordinate $\alpha$, so the extension requirement is automatic from the induction hypothesis at $\alpha$. At limit coordinates, the finite-support definition of the iteration says that a condition and the order are determined by all earlier restrictions, so the induction passes to the limit. Therefore $s\in P_\lambda$ and $s$ is a common strengthening of $p_\xi$ and $p_\eta$ in $P_\lambda$.[/guided]

[step:Conclude the limit case and the induction] The condition $s$ constructed above is a common strengthening of two distinct members $p_\xi,p_\eta\in A$. This contradicts the assumption that $A$ is an antichain in $P_\lambda$. Therefore $P_\lambda$ is ccc at every limit stage $\lambda\leq\kappa$. By transfinite induction, $P_\lambda$ is ccc for every $\lambda\leq\kappa$. In particular, $P_\kappa$ is ccc. [/step]