Generic extensions satisfy ZF and preserve ground-model Choice

F2 and F4 give transitivity and the stated containments. Empty Set and Infinity hold since the actual empty set and omega belong to M and hence to M[G]. Extensionality holds in a transitive domain: every member of either set is in that domain. For Foundation, any nonempty $x\in M[G]$ has an ambient membership-minimal $y\in x$; transitivity puts y in M[G], and $y\cap x=\mathrm{\varnothing }$ remains true there. F3 constructs an unordered pair name $S(\{\sigma ,\tau \})$, giving Pairing.

For Separation, let $a={\sigma }_G$ and let $\vec{b}={\vec{\tau }}_G$ be the parameters of a fixed formula $\phi$. Put $T=\mathrm{dom}(\sigma )$ and form in M the name $\eta =\{⟨\rho ,p⟩\in T\times P:p{⊩}^M(\rho \in \sigma \wedge \phi (\rho ,\vec{\tau }))\}$. It is a set by internal Separation using definability in F1. A member of its value satisfies the displayed conjunction by the truth lemma. Conversely any $x\in a$ has a representative $\rho \in T$; if $\phi (x,\vec{b})$ holds, the truth lemma supplies a p in G for that conjunction. Hence ${\eta }_G=\{x\in a:M[G]\models \phi (x,\vec{b})\}$, proving every Separation instance.

For Union, for $a={\sigma }_G$ form $T={\bigcup }_{\rho \in \mathrm{dom}(\sigma )}\mathrm{dom}(\rho )$ in M. F3 gives $u=S(T{)}_G\in M[G]$. If $z\in y\in a$, valuation first gives a subname $\rho$ of sigma for y and then a subname of rho for z, so $z\in u$. Separation from step 1.2, with predicate $\mathrm{\exists }y\in a(z\in y)$, cuts out exactly $\bigcup a$ from u.

For Replacement, suppose a fixed formula $\phi (x,y,\vec{b})$ defines exactly one y for every $x\in a={\sigma }_G$. For each $(\rho ,p)\in \mathrm{dom}(\sigma )\times P$, define in M $\gamma (\rho ,p)$ to be the least ordinal $\gamma$ for which some name $\tau \in V_{\gamma }^M$ has $p{⊩}^M\phi (\rho ,\tau ,\vec{\tau })$; put it equal to zero if there is no such name. This is a definable ordinal function, so internal Replacement gives an ordinal $\delta$ strictly above every such $\gamma$. Internal Separation forms the set U of names in $V_{\delta }^M$. F3 gives $u=S(U{)}_G\in M[G]$. Given $x\in a$ and its unique y, choose a representing subname rho for x and any name for y. F1 gives p in G forcing the matrix. By the definition of the least rank, there is a witnessing name in U forced by that same p; F1 and uniqueness identify its value with y. Thus u contains every output. Separation using $\mathrm{\exists }x\in a\phi (x,y,\vec{b})$ gives the exact range. Only least ranks were collected, never a chosen name from each witness class.

For Power Set, put $T=\mathrm{dom}(\sigma )$ for $a={\sigma }_G$ and form $Q=\mathcal{P}(T\times P{)}^M$ in M. Every element of Q is a name, so $u=S(Q{)}_G$ belongs to M[G]. If $y\in M[G]$ and $y\subseteq a$, choose a name eta for y and form $\theta =\{⟨\rho ,p⟩\in T\times P:p{⊩}^M\rho \in \eta \}\in Q$. By F1 its value is contained in y. Conversely a member x of y is in a and has a representative rho in T; the truth lemma supplies p in G forcing its membership in eta, so x is in ${\theta }_G$. Thus $y={\theta }_G\in u$. Separation of u by $y\subseteq a$ now gives exactly the internal power set of a. This uses only M's subsets of $T\times P$, not its external power set.

The preceding steps give every axiom of ZF: the elementary axioms, Union, each Separation and Replacement instance, and Power Set. The target instances were derived from fixed internal forcing predicates; no truth predicate for M[G] was assumed inside M. This establishes the entire ZF branch.

Assume now, only for this branch, that M satisfies AC. Given $a={\sigma }_G$, F5–F7 inside M provide a bijection $h:\xi \to \mathrm{dom}(\sigma )$ for some ordinal xi; this is the exact use of ground-model AC. F3 constructs in M a graph name whose value in M[G] is the function $f(i)=h(i{)}_G$ on xi. Its range covers a. In the ZF model from step 3.1, for each $x\in a$ the nonempty fibre $\{i<\xi :f(i)=x\}$ has a least ordinal. Least fibres inject a into xi and well-order a. For a family of nonempty sets in M[G], apply this to its union and take the least member of each family member; target Replacement yields the choice function. Empty a and the empty family need only the empty maps. Thus M[G] satisfies AC, with no ambient AC assumption.