Kunen inconsistency with atoms

Question

Kunen showed that there is no nontrivial $j: V \rightarrow_e V$. One might wonder what happens in $\mathsf{ZFC}$ with atoms.

Let's denote the universe by $U$. We aren't assuming that the atoms form a set, or even that there are no more atoms than pure sets. Of course, if there at least two atoms, there will be nontrivial automorphisms on $U$, so that isn't very interesting. The following seems like a better way of translating Kunen's question into this framework: let's call an elementary embedding atrivial if it is nontrivial but it is the identity mapping on atoms. Can there be an atrivial $j: U \rightarrow_e U$?

Two comments: 1) I've tried to prove that there can be no such $j$ by, in essence, quotienting out distinctions among Urelemente (similar to a Fraenkel-Mostowski model) and building a $j'$ that inherits nontriviality, but without success; 2) note that every object has at most set-many atoms in its transitive closure, so one can find a set of atoms $A$ such that $j$ is nontrivial on the restricted hierarchy $U(A)$ built over those atoms alone; unfortunately, there's no guarantee that $j``U(A)$ is a class built up only over set-many atoms.

Answer 1

Theorem. The Kunen inconsistency works over ZFC with atoms. That is, in this theory, there is no non-identity elementary embedding $j:V\to V$ that fixes every atom.

Proof. Suppose that $j:V\to V$ is an elementary embedding fixing every atom. If $j$ is not the identity embedding, then I claim that $j$ must move an ordinal. To see this, let $u$ be any $\in$-minimal element that is moved by $j$. Let us well-order $u$ in some order type $\beta$. Since ordinals are fixed by $j$, it follows that the $\alpha^{th}$ element of $u$ is carried by $j$ to the $j(\alpha)^{th}=\alpha^{th}$ element of $j(u)$, but since those elements are fixed (by minimality of $u$) and the total length of the well-order is fixed, it follows that $j(u)$ is simply $u$ itself, contradicting the choice of $u$. (In fact, by an argument on ranks, one can eliminate the use of choice in this part of the argument; but you still need it for the other part.)

So $j$ is not the identity on ordinals. We may now restrict $j$ to the pure part of the universe. Let $W$ be the class of sets having no atoms in their transitive closures. This is a model of ZFC, without atoms. Since this is definable, it follows that $j\upharpoonright W$ is a nontrivial elementary embedding from $W$ to $W$. This contradicts the usual Kunen inconsistency. For example, one gets that $j\upharpoonright V_{\lambda+2}^W$ is a set in $W$, where $\lambda$ is the supremum of the critical sequence, and this violates the usual ZFC version of the Kunen inconsistency in $W$. $\Box$