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

Cohen's forcing poset $\mathbb{P} = \mathrm{Fn}(\aleph_2 \times \omega, 2)$ consists of all finite partial functions $p$ from $\aleph_2 \times \omega$ into $\{0,1\}$ (a "condition" fixes finitely many bits, indexed by which of the $\aleph_2$ sequences and which position in it), ordered by reverse inclusion: $q \le p$ ("$q$ is stronger") exactly when $q \supseteq p$, i.e. $q$ agrees with $p$ wherever $p$ is defined and decides strictly more.

A filter $G \subseteq \mathbb{P}$ is generic (over a ground model $V$) if it meets every dense subset of $\mathbb{P}$ that belongs to $V$ — informally, $G$ eventually answers every question about the sequences that could be asked using only information already in $V$. Cohen (1963, 1964) showed such generic filters exist (by a Rasiowa–Sikorski style argument, since $V$ only has countably many dense sets to worry about relative to $\mathbb{P}$, when working one real at a time) and that $f_G = \bigcup_{p \in G} p$ assembles into $\aleph_2$ genuinely new total binary sequences, i.e. new real numbers, forming the generic extension $V[G]$.

Because $G$ itself is deliberately chosen from outside $V$, $V[G]$ strictly extends $V$ with new sets while keeping every old set of $V$ intact. The next step shows $V[G]$ still satisfies all of $\mathrm{ZFC}$, and that these $\aleph_2$ new reals are forced to be genuinely distinct from each other.