= Basic Fraenkel permutation model
{c}
Start with a well-founded universe of <sets> over an infinite set $A$ of <urelements>. The full <symmetric group> of $A$ acts recursively on sets. Retain the objects all of whose descendants have a <finite support in a permutation action>. This class satisfies set-extensionality, <foundation>, <infinity>, <pairing>, <union>, <separation>, <replacement> and its internal <power set> axiom. A definable functional image has the finite union of the supports of its domain and parameters as a support; uniqueness makes the image invariant. The family of two-element subsets of $A$ has no <choice function>: a transposition of two atoms outside the function's finite support fixes their pair and moves either possible choice. For untyped membership with extensionality merely restricted to nonempty objects, atoms are also vacuous subsets; add all atoms to each internal power-set object.
Back to article page
