Worked solution: Gödel and Cohen: the continuum hypothesis is independent of ZFC (1963)

A general theorem about forcing (proved by Cohen alongside the construction itself) says: whenever $G$ is generic over a model $V$ of $\mathrm{ZFC}$, the extension $V[G]$ again satisfies every $\mathrm{ZFC}$ axiom — forcing extensions never break the basic rules of set theory, they only add new sets.

Genericity also guarantees that for any two distinct coordinates $\xi \ne \eta$ below $\aleph_2$, the set of conditions that force the $\xi$-th and $\eta$-th sequences to disagree somewhere is dense (given any finite condition, one can always extend it to record a disagreement at some fresh, unused position), so $G$ must meet it. Hence the $\aleph_2$ real numbers $r_\xi = \{ n : f_G(\xi, n) = 1 \}$ for $\xi < \aleph_2$ are pairwise distinct, giving at least $\aleph_2$ reals in $V[G]$, i.e. $2^{\aleph_0} \ge \aleph_2$ there.

This already looks like it refutes $\mathrm{CH}$, but there is a subtlety: the argument only shows $\aleph_2$-many reals exist, which refutes $\mathrm{CH}$ only if $\aleph_1$ and $\aleph_2$ from the ground model $V$ are still genuinely $\aleph_1$ and $\aleph_2$ in $V[G]$ — if forcing had secretly collapsed them, "$\aleph_2$-many reals" might really just be $\aleph_1$-many in disguise. The next step closes this gap.