A Universe of Sorts

These are used to show create models of ZF + not(Choice).
Key idea: if we just have ZF without atoms, then a set has no non-trivial ∈ preserving permutations.
Key idea: if we have atoms, then we can permute the atoms to find non-trivial automorphisms of our model.
Key idea: in ZF + atoms, the ordinals come from the ZF fragment, where they live in the kernel [ie the universe formed by repeated application of powerset to the emptyset ]. Thus, the "order theory" of ZF + atoms is controlled by the ZF fragment.
Crucially, this means that the notion of "well ordered" [ie, in bijection with ordinal ] is determined by the ZF fragment.
Now suppose (for CONTRADICTION) that A is well ordered. This means that we Now suppose we have an injection f: ordinal -> A where A is our set of atoms.
Since A possesses non-trivial structure preserving automorphisms, so too must ordinal, since ordinal is a subset of A. But this violates the fact that ordinal cannot posses a non-trivial automorphism.
Thus, we have contradiction. Ths means that A cannot be well-ordered, ie, there cannot be an injection f: ordinal -> A.

§ Permutation Models