This is an attempt to locate a theorem I vaguely remember but cannot find (which arose in the context of [Consistency of non-trivial elementary embedding $j : \mathit{Ord} \to \mathit{Ord}$](https://math.stackexchange.com/q/3947955/28111) and motivated https://mathoverflow.net/questions/378918/can-ord-have-nontrivial-second-order-elementary-self-embeddings). Specifically, I recall a theorem along the following lines (in contrast of course with the Kunen inconsistency): > Every "reasonably definable" expansion of the class-sized structure $(\mathit{Ord}; \in)$ has nontrivial elementary self-embeddings. Here the relevant notion of "reasonably definable" was broad enough to include the usual ordinal arithmetic operations, and if I recall correctly more complicated operations like $\alpha\mapsto\omega_\alpha$. On the other hand, it was a $\mathsf{ZFC}$ theorem, so we certainly can't go all the way to second-order logic (see [the MO question linked above](https://mathoverflow.net/questions/378918/can-ord-have-nontrivial-second-order-elementary-self-embeddings)). Additionally, I vaguely recall that this was due to either Harvey Friedman or Mostowski and that the relevant definability notion was "least-fixed-point-flavored," but I'm much less confident about either of these memories.