 (where \(\in\) is the membership relation of the nonstandard model). The proof that this is a model of NFU is not long, but it is involved enough that we refer the reader elsewhere. The basic idea is that the automorphism allows us to code the (apparent) power set \(V_{\alpha +1}\) of our universe \(V_{\alpha}\) into the “smaller” \(V_{j(\alpha)+1}\) which is included in our universe; the left over objects in \(V_{\alpha} - V_{j(\alpha)+1}\) become urelements. Note that \(V_{\alpha} - V_{j(\alpha)+1}\) is most of the domain of the model of NFU in a quite strong sense: almost all of the universe is made up of urelements (note that each \(V_{\beta +1}\) is the power set of \(V_{\beta}\), and so is strictly larger in size, and not one but many stages intervene between \(V_{j(\alpha)+1}\) (the collection of “sets”) and \(V_{\alpha}\) (the “universe”)). This construction is related to the construction used by Jensen, but is apparently first described explicitly in Boffa 1988.