= Solution
Work in a ground <first-order model> of <set theory> satisfying <ZF>, and let $\pi$ be a definable <bijection> of its universe, whose inverse is also definable. Write $\psi=\pi^{-1}$ and replace membership by
$$
x\mathrel E y\quad\Longleftrightarrow\quad x\in\pi(y).
$$
In this <Rieger-Bernays permutation model>, an object having prescribed extension $b$ is represented by $\psi(b)$. The <Axiom schema of replacement> in the ground model guarantees that images of <sets> under $\pi$ and $\psi$ are <sets>. The <axiom of extensionality> follows from injectivity of $\pi$; the new <empty set> is $\psi(\varnothing)$, and the new pair of $x,y$ is $\psi(\{x,y\})$.
For the <Axiom of union> and <Axiom of power set>, representatives are respectively
$$
\psi\left(\bigcup_{y\in\pi(x)}\pi(y)\right),\qquad
\psi\left(\{\psi(s):s\subseteq\pi(x)\}\right).
$$
Indeed, $z$ is an $E$-subset of $x$ exactly when $\pi(z)\subseteq\pi(x)$. Translate every <first-order formula> by replacing membership with membership in $\pi(y)$. Ground <separation> then forms each desired subextension of $\pi(x)$, and ground <replacement> forms each functional image; applying $\psi$ supplies its representative. To verify the <axiom of infinity>, define by ground recursion
$$
a_0=\psi(\varnothing),\qquad a_{n+1}=\psi(\pi(a_n)\cup\{a_n\}).
$$
Then $\psi(\{a_n:n<\omega\})$ is an $E$-inductive <set>. Thus every <ZF> axiom except possibly the <Axiom of foundation> survives.
Interchange two distinct objects $a$ and $\{a\}$, fixing everything else. Then $\pi(a)=\{a\}$, so $a$ is a <Quine atom>: internally $a=\{a\}$. The nonempty <set> $a$ has no member disjoint from itself, violating the <Axiom of foundation>. The original membership model satisfies that axiom. \b[<Foundation> is therefore relatively independent of the other <ZF> axioms.]
A full <Rieger-Bernays permutation model> of a choice model still satisfies the <axiom of choice>: choose an old member of each nonempty extension $\pi(y)$ and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.
Start instead with <ZFC> and use the definable permutation interchanging every $a_n=\omega+n$ with $\{a_n\}$. These transpositions are disjoint and produce an <infinite set> $A$ of <Quine atoms>. Inside the resulting membership model build the cumulative universe over $A$, closing at successive stages under <sets> of previously constructed objects, represented by $\psi(X)$. Atomic objects are kept as the designated base objects; $\psi(\{a\})=a$ for $a\in A$. Every permutation of $A$ extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.
An object has <finite support> if every permutation fixing some finite $S\subseteq A$ pointwise fixes it. Retain the objects which have <finite support> and whose members recursively also have <finite support>, interpreting the atomic self-loops as the base case. This is the <hereditarily finite-supported Quine-atom model>. It is transitive for the new membership relation. <Extensionality> is inherited. Pairs and <unions> have supports contained in the <union> of the finitely many relevant supports. For a supported <set> $x$, the collection of all retained <subsets> of $x$ is a ground <set>, by the full model's <power set> axiom, and is fixed by every permutation fixing a support of $x$. Its members are retained, so this collection supplies the internal <power set>. A <first-order formula> with retained parameters is invariant under their common stabilizer. Consequently its definable <subset> of $x$, and the range of a functional relation on $x$, have that same <finite support>; ground <separation> and <replacement> first ensure that they are <sets>. The pure natural-number hierarchy supplies <infinity>. These arguments verify all of <ZF> except <Axiom of foundation>, which fails at the <Quine atoms>.
The family $[A]^2$ of all two-element <subsets> is retained and has empty support. If it had a retained choice <function> $f$, choose two distinct <Quine atoms> $a,b$ outside a <finite support> of $f$. The transposition of $a,b$ fixes $f$ and fixes the unordered pair $\{a,b\}$, but moves either possible value $f(\{a,b\})$. This is impossible. Thus \b[<ZF> without <Foundation> has both choice models and models in which Choice fails], relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.
Back to article page
