Fraenkel–Mostowski permutation-model theorem

Every atom is symmetric because ${\mathrm{fix}}_G(\{a\})$ fixes $a$, and every pure set is fixed by every permutation; both are hereditarily symmetric, so $A\cup K\subseteq \mathrm{H}\mathrm{S}$, while conversely the pure kernel is unchanged because no atom lies in a pure set. Transitivity is F1. Empty Set, Infinity, Extensionality and Foundation restrict from $M$. If $x,y\in \mathrm{H}\mathrm{S}$, the stabilizer intersection fixes $\{x,y\}$, $x\cup y$, and the usual finite set operations; their members are hereditary, giving Pairing and Union.

Because $G,\mathcal{F}$ and their action are internal to $M$, the predicate “$u\in {\mathrm{H}\mathrm{S}}_{\mathcal{F}}^M$” is definable over $M$ from those parameters by rank recursion. Hence $M$-Separation forms $z=\{u\in {\mathcal{P}}^M(x):M\models u\in {\mathrm{H}\mathrm{S}}_{\mathcal{F}}\}\mathrm{.}$ Every permutation fixing $x$ maps $z$ to itself because hereditary symmetry is invariant; all members are HS, so $z\in \mathrm{H}\mathrm{S}$ and it is exactly the internal power set. For Separation with supported parameters, formula invariance shows the defining subset of $x$ has the intersection of their stabilizers as support.

For Replacement, suppose the internal formula assigns a unique $y$ to every $x\in a$. Ambient Replacement forms the image $b$. Any permutation fixing $a$ and all parameters maps a witnessed pair $(x,y)$ to $(gx,gy)$; uniqueness therefore maps $b$ to itself. Each value $y$ is in HS by the internal quantifier domain, so $b$ is hereditarily symmetric. This proves every ZFA axiom without Choice.

Noninheritance is witnessed by the finite-support full-permutation system on a countably infinite atom set: its atom set is HS, but a supported well-order would be moved by a transposition outside its finite support. Thus the ambient $M$ may satisfy F2 while its HS submodel does not.