Hereditarily symmetric interpretations form a transitive ZF model

Values of HS names lie in $M[G_0]$, while hereditary closure says that every member of such a value has an HS subname. Hence $M\subseteq N\subseteq M[G_0]$ and $N$ is transitive.

The class is almost universal relative to the ambient transitive ZF extension $M[G_0]$, without choosing simultaneous HS representatives. Let $\dot{x}\in M$ name an ambient set $x\subseteq N$. For each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$, define $r(\tau ,p)$ to be the least ordinal rank of an HS name $\sigma$ for which $p⊩\tau =\sigma$, if there is one, and $0$ otherwise. This is a definable ground-model function: the forcing relation and the HS predicate are definable, and any nonempty definable class of ordinal ranks has a least member. ZF Replacement in $M$ strictly bounds its values on the displayed set by an ordinal $\alpha$. If $u\in x$, some $(\tau ,p)\in \dot{x}$ has $p\in G_0$ and ${\tau }_{G_0}=u$; since $u\in N$, some HS $\sigma$ also evaluates to $u$. The truth lemma gives a common strengthening $q\in G_0$ of $p$ forcing $\tau =\sigma$, so $r(\tau ,q)<\alpha$. Thus every $u\in x$ is the value of an HS name of rank below $\alpha$.

For $a,\vec{w}\in N$ and a bounded formula $\phi (u,\vec{w})$ with any finite tuple of parameters, choose HS names $\dot{a},\dot{\vec{w}}$ and form the ground set-name $\{(\tau ,p)\in \mathrm{dom}(\dot{a})\times P:p⊩\tau \in \dot{a}\wedge \phi (\tau ,\dot{\vec{w}})\}$. Every immediate subname $\tau$ of $\dot{a}$ is HS. Bounded truth is absolute between the transitive classes $N$ and $M[G_0]$, so the truth lemma evaluates this name to $\{u\in a:N\models \phi (u,\vec{w})\}$. F2 shows that the finite intersection of the parameter stabilizers fixes this name, whose subnames are HS; filter closure puts that intersection in the filter. Thus $N$ has every instance of ${\mathrm{\Delta }}_0$-Separation.

Apply Jech's transitive-class criterion inside $M[G_0]$, rather than cutting an arbitrary ambient subset by bounded Separation. Transitivity supplies Extensionality and Foundation; check names supply $\mathrm{\varnothing }$ and $\omega$. For $N$-parameters, each of Jech's eight Gödel-operation outputs—unordered pair, difference, product, domain, membership relation restricted to a square, and three coordinate permutations—is an ambient set of elements already in $N$: first use unordered pairs and Kuratowski pairs, then the remaining operations in that finite order. By step 1.2 each such output lies inside an $N$-set, and its defining bounded formula with those parameters lets step 1.3 cut out exactly the output. Hence $N$ is closed under the eight operations. Jech's formula-complexity induction from that closure and almost universality gives full Comprehension, including the unbounded-quantifier cases; it also derives Pairing, Union, internal Power Set, Infinity and Replacement (the last by bounding the outer set of functional values via almost universality, then applying Comprehension). This proves every ZF schema instance. No AC enters this argument, and only the ZF branch of F3 is used.