Gitik's symmetric submodel satisfies ZF

By F2, every finite tuple of members of $N_G$ lies in one $N_{G_{\theta }}$. The restricted forcing and symmetry data form a set-sized symmetric system, so F5 makes each such stage a transitive ZF model. The inclusions between stages preserve membership, and F2 therefore makes their union transitive. Check names put every ground set, in particular $\mathrm{\varnothing }$ and $\omega$, in every sufficiently large stage. Extensionality and Foundation are absolute to the transitive union, while Pairing, Union and Infinity may be computed in one common stage and have the same values in the union.

Fix $x\in N_G$ and let $S_x$ be the set supplied by F4 inside $M[G]$. For each $y\in S_x$, F3 gives a regular $\theta$ with $y\in N_{G_{\theta }}$; use F1's definable global well-order to take the least such $\theta$. Collection in $M[G]$ bounds these stages by one regular $\mathrm{\Theta }$, enlarged if necessary so that $x\in N_{G_{\mathrm{\Theta }}}$. Thus $S_x\subseteq N_{G_{\mathrm{\Theta }}}$. Conversely every $y\in N_{G_{\mathrm{\Theta }}}$ with $y\subseteq x$ belongs to $N_G$, so transitivity gives $S_x={\mathcal{P}}^{N_{G_{\mathrm{\Theta }}}}(x)\mathrm{.}$ The right side is a member of $N_{G_{\mathrm{\Theta }}}$ by F5 and hence of $N_G$. This proves Power Set in $N_G$. If $x=\mathrm{\varnothing }$, both sides are the singleton $\{\mathrm{\varnothing }\}$, so the argument includes the empty endpoint.

In the ambient $M[G]$, recursively form $R_{\alpha }^N=\{u\in N_G:\mathrm{rank}(u)<\alpha \}$. The recursion is set-valued without ambient Power Set. At a successor, $R_{\alpha +1}^N={\mathcal{P}}^{N_G}(R_{\alpha }^N)$ is the set given by step 1.2. At a limit $\lambda$, Replacement and Union in F1 form ${\bigcup }_{\alpha <\lambda }{R}_{\alpha }^N$. To see that this limit set belongs to $N_G$, apply F3 and Collection to its members, bounding them in one stage $N_{G_{\mathrm{\Theta }}}$. That stage is transitive and has exactly the same members of rank below $\lambda$, so $R_{\lambda }^N=R_{\lambda }^{N_{G_{\mathrm{\Theta }}}}\in N_{G_{\mathrm{\Theta }}}$. The zero case is empty and successor stages are already in $N_G$ by step 1.2. Thus every $R_{\alpha }^N$ is a set of $M[G]$ and a member of $N_G$.

The class $N_G$ is almost universal relative to $M[G]$. Indeed, if $a\in M[G]$ and $a\subseteq N_G$, Replacement in F1 collects the ranks of members of $a$. For an ordinal $\alpha$ strictly above their supremum, $a\subseteq R_{\alpha }^N$, and step 2.1 gives $R_{\alpha }^N\in N_G$. This argument bounds the whole ambient set at once; it does not choose names or supports for its members.

Bounded Separation holds in $N_G$. Given $a,\vec{z}\in N_G$ and a bounded formula, choose one stage containing the finite tuple. Bounded truth is absolute between the transitive models $N_{G_{\theta }}$ and $N_G$, so Separation in that stage gives the required subset of $a$. The same argument constructs unordered pairs and the boundedly definable parts of each of Jech's eight Gödel operations. More generally, an operation output formed in $M[G]$ from $N_G$-parameters is an ambient set of elements of $N_G$; step 3.1 places it inside an $N_G$-set, and bounded Separation cuts out its exact value. Hence $N_G$ is closed under unordered pair, difference, product, domain, membership restricted to a square and the three permutations of triple coordinates.

Continue by induction on formula complexity, using only the transitivity, almost universality and bounded cuts already verified. Atomic and Boolean cuts use step 4.1. At an existential step, for every tuple in the current argument set, first take the least rank of an $N_G$-witness when one exists and then use F1's ambient definable global well-order on that set-sized rank segment to select a least witness. Replacement in F1 collects these witnesses, step 3.1 places them in an $N_G$-container, and projection of the lower-complexity relation gives the existential cut. This proves every Separation instance. For a functional formula on $a\in N_G$, the same ambient Replacement collects its unique $N_G$-values, almost universality gives an $N_G$-container, and the just-proved Separation instance cuts out exactly the range, proving Replacement. Together with steps 1.1 and 1.2 this is all of ZF. F6 records only the upstream ground choices; the proof never invokes AC in $M[G]$ or constructs a choice function in $N_G$.