= Solution
Let $x=\tau_G$ be any <set> in the extension. The <set> $D=\{\sigma:\exists p\ ((\sigma,p)\in\tau)\}$ belongs to $M$. Ground-model choice <well-orders> it, so fix an enumeration $\langle\sigma_\xi:\xi<\theta\rangle$ by an <ordinal> in $M$. In $M[G]$, take
$$
I=\{\xi<\theta:\exists p\in G\ ((\sigma_\xi,p)\in\tau)\}.
$$
Evaluation gives a <surjection> $\xi\mapsto(\sigma_\xi)_G$ from $I$ onto $x$. This is a <set> <function> by the <ZF> part of the <forcing theorem>; no extension choice is needed. For each $y\in x$, take its least preimage <ordinal>. Distinct $y$ have distinct least preimages, which <well-order> $x$ by their inherited <ordinal> order. Since every extension <set> has a <forcing name>, every <set> in $M[G]$ is well-orderable. Therefore
$$
\boxed{M[G]\models\mathrm{AC}.}
$$
This <choice preservation by well-ordered names> tolerates repeated evaluations, because the least-index step removes them canonically.
Back to article page
