Choice preservation by well-ordered names (source code)

= Choice preservation by well-ordered names
{title2=$M\models\mathrm{AC}\Longrightarrow M[G]\models\mathrm{AC}$}

If the ground model has <axiom of choice>, <well-order> the <set> of subnames appearing in a <forcing name> for an arbitrary extension <set>. Evaluate those activated by the <generic filter>. Each element of the extension <set> has a least preimage index; ordering by these indices <well-orders> the <set>. Only ground choice and the <ZF> part of the <forcing theorem> are needed.