[proofplan] The [forcing theorem](/theorems/6531) gives that the generic extension $M[G]$ satisfies $\mathrm{ZFC}$. The key point is that $\operatorname{Add}(\omega,\omega_2^M)^M$ has the countable chain condition in $M$, so it preserves $\omega_1^M$ and $\omega_2^M$ as cardinals. The generic filter simultaneously adds one Cohen real at each coordinate $\alpha<\omega_2^M$, and a density argument separates the reals at distinct coordinates. Hence $M[G]$ contains at least $\omega_2^M$ many reals, while $\omega_1^M$ is still the first uncountable cardinal, so the continuum is not $\omega_1$. [/proofplan]

[step:Use the forcing theorem to obtain a model of $\mathrm{ZFC}$] Let $\kappa=(\omega_2)^M$. Since $M\models\mathrm{ZFC}$ and $\mathbb P\in M$ is a forcing notion, the forcing theorem for set forcing implies that the $M$-generic extension $M[G]$ is a transitive model of $\mathrm{ZFC}$ containing $M$ and $G$ (citing a result not yet in the wiki: Forcing Theorem). Thus it remains only to prove that $M[G]\models\neg\mathrm{CH}$. [/step]

[step:Prove in $M$ that $\mathbb P$ has the countable chain condition]We show that $M$ satisfies that every antichain in $\mathbb P$ is countable. Let $A\in M$ be an antichain in $\mathbb P$. Since each $p\in A$ is a finite partial function $p:\kappa\times\omega\to 2$, define its support \begin{align*} \operatorname{supp}(p)=\{\alpha<\kappa:\text{ there exists } n\in\omega \text{ with } (\alpha,n)\in\operatorname{dom}(p)\}. \end{align*} This is a finite subset of $\kappa$. Suppose, toward a contradiction inside $M$, that $A$ is uncountable. Applying the delta-system lemma in $M$ to the uncountable family $\{\operatorname{supp}(p):p\in A\}$, there is an uncountable subset $A_0\subseteq A$ and a finite set $r\subseteq\kappa$ such that \begin{align*} \operatorname{supp}(p)\cap\operatorname{supp}(q)=r \end{align*} for all distinct $p,q\in A_0$. There are only countably many finite partial functions from $r\times\omega$ to $2$, because $r\times\omega$ is countable and each finite domain has only finitely many $2$-valued functions. Hence, by thinning $A_0$ further inside $M$, there is an uncountable set $A_1\subseteq A_0$ and a fixed finite partial function $s:r\times\omega\to 2$ such that \begin{align*} p\big|_{r\times\omega}=s \end{align*} for every $p\in A_1$. Choose distinct $p,q\in A_1$. Their domains may overlap only on $r\times\omega$, and on this common part they agree with the same function $s$. Therefore $p\cup q$ is a finite partial function from $\kappa\times\omega$ to $2$, so $p\cup q\in\mathbb P$. Since the order on $\mathbb P$ is reverse inclusion, $p\cup q\leq p$ and $p\cup q\leq q$. Thus $p$ and $q$ are compatible, contradicting that $A$ is an antichain. Therefore every antichain in $\mathbb P$ belonging to $M$ is countable in $M$.[/step]

[guided]We need the countable chain condition because it is the preservation mechanism for the relevant cardinals. Let $A\in M$ be an antichain in $\mathbb P$. A condition $p\in\mathbb P$ is a finite partial function \begin{align*} p:\kappa\times\omega\to 2. \end{align*} The coordinate support of $p$ is the finite set \begin{align*} \operatorname{supp}(p)=\{\alpha<\kappa:\text{ there exists } n\in\omega \text{ with } (\alpha,n)\in\operatorname{dom}(p)\}. \end{align*} Assume, for contradiction, that $A$ is uncountable in $M$. The family of supports \begin{align*} \{\operatorname{supp}(p):p\in A\} \end{align*} is an uncountable family of finite sets in $M$. By the delta-system lemma, applied in $M$, there are an uncountable subset $A_0\subseteq A$ and a finite root $r\subseteq\kappa$ such that any two distinct supports in $A_0$ intersect exactly in $r$: \begin{align*} \operatorname{supp}(p)\cap\operatorname{supp}(q)=r. \end{align*} This does not yet make two conditions compatible, because two conditions could still disagree on the coordinates in the common root. We now remove that obstruction. Since $r$ is finite, $r\times\omega$ is countable. There are only countably many finite partial functions from $r\times\omega$ to $2$. Since $A_0$ is uncountable, one restriction pattern occurs uncountably often. Thus there are an uncountable $A_1\subseteq A_0$ and a fixed finite partial function $s:r\times\omega\to 2$ such that \begin{align*} p\big|_{r\times\omega}=s \end{align*} for every $p\in A_1$. Now take distinct $p,q\in A_1$. Outside $r\times\omega$, their domains lie on disjoint coordinate supports. On $r\times\omega$, both restrictions are equal to $s$. Hence there is no point of the common domain at which $p$ and $q$ assign different values. Therefore $p\cup q$ is a finite partial function from $\kappa\times\omega$ to $2$, so $p\cup q\in\mathbb P$. Since $\mathbb P$ is ordered by reverse inclusion, $p\cup q$ extends both conditions: \begin{align*} p\cup q\leq p \end{align*} and \begin{align*} p\cup q\leq q. \end{align*} Thus $p$ and $q$ are compatible, contradicting that $A$ was an antichain. The contradiction proves that $M$ satisfies the countable chain condition for $\mathbb P$.[/guided]

[step:Preserve $\omega_1^M$ and $\omega_2^M$ in the generic extension] Since $M\models\mathbb P$ is ccc, the standard preservation theorem for ccc forcing implies that forcing with $\mathbb P$ preserves uncountable cardinals and cofinalities of $M$ (citing a result not yet in the wiki: ccc forcing preserves cardinals). In particular, \begin{align*} (\omega_1)^{M[G]}=(\omega_1)^M \end{align*} and $\kappa=(\omega_2)^M$ remains a cardinal in $M[G]$. Therefore, in $M[G]$, \begin{align*} (\omega_1)^{M[G]}<\kappa. \end{align*} [/step]

[step:Extract one Cohen real from each coordinate] For each $\alpha<\kappa$, define the function \begin{align*} c_\alpha:\omega\to 2 \end{align*} in $M[G]$ by \begin{align*} c_\alpha(n)=i \iff \text{there exists } p\in G \text{ such that } p(\alpha,n)=i. \end{align*} This is well-defined because any two conditions in the filter $G$ are compatible, so they cannot assign different values to the same point $(\alpha,n)$. For each $n\in\omega$, the set \begin{align*} D_{\alpha,n}=\{p\in\mathbb P:(\alpha,n)\in\operatorname{dom}(p)\} \end{align*} is dense in $\mathbb P$: given $p\in\mathbb P$, if $(\alpha,n)\in\operatorname{dom}(p)$ then $p\in D_{\alpha,n}$; otherwise $p\cup\{((\alpha,n),0)\}$ is a condition extending $p$ and belongs to $D_{\alpha,n}$. Since $D_{\alpha,n}\in M$ and $G$ is $M$-generic, $G\cap D_{\alpha,n}\neq\varnothing$. Hence $c_\alpha(n)$ is defined for every $n\in\omega$, so $c_\alpha\in 2^\omega$ in $M[G]$. [/step]

[step:Separate the Cohen reals at distinct coordinates] Let $\alpha,\beta<\kappa$ with $\alpha\neq\beta$. Define \begin{align*} E_{\alpha,\beta}=\{p\in\mathbb P:\text{ there exists } n\in\omega \text{ such that } p(\alpha,n)\neq p(\beta,n)\}. \end{align*} The set $E_{\alpha,\beta}$ is dense in $\mathbb P$. Indeed, given $p\in\mathbb P$, choose $n\in\omega$ such that neither $(\alpha,n)$ nor $(\beta,n)$ belongs to $\operatorname{dom}(p)$; this is possible because $\operatorname{dom}(p)$ is finite. Then \begin{align*} q=p\cup\{((\alpha,n),0),((\beta,n),1)\} \end{align*} is a finite partial function from $\kappa\times\omega$ to $2$, so $q\in\mathbb P$, and $q\leq p$. Also $q\in E_{\alpha,\beta}$. Since $E_{\alpha,\beta}\in M$ and $G$ is $M$-generic, choose $p\in G\cap E_{\alpha,\beta}$. Then for some $n\in\omega$, \begin{align*} p(\alpha,n)\neq p(\beta,n). \end{align*} By the definition of $c_\alpha$ and $c_\beta$, this gives \begin{align*} c_\alpha(n)\neq c_\beta(n). \end{align*} Therefore $c_\alpha\neq c_\beta$. [/step]

[step:Conclude that the continuum is larger than $\omega_1$] Define the map \begin{align*} F:\kappa\to 2^\omega \end{align*} in $M[G]$ by \begin{align*} F(\alpha)=c_\alpha. \end{align*} The previous step proves that $F$ is injective. Therefore, in $M[G]$, \begin{align*} \kappa\leq |2^\omega|. \end{align*} Since $\kappa=(\omega_2)^M$ remains a cardinal and $(\omega_1)^{M[G]}=(\omega_1)^M<\kappa$, we have \begin{align*} (\omega_1)^{M[G]}<|2^\omega|^{M[G]}. \end{align*} Thus $M[G]\models 2^{\aleph_0}>\aleph_1$, and hence $M[G]\models\neg\mathrm{CH}$. Combining this with the first step, we obtain \begin{align*} M[G]\models\mathrm{ZFC}+\neg\mathrm{CH}. \end{align*} [/step]