While at Luminy, David Asperó showed me a quick proof of a nice result on Reinhardt cardinals in . It complements Grigor Sargsyan’s result discussed here.
Theorem (Asperó). Work in
. Suppose
is a nontrivial elementary embedding. Then there are a
and an ordinal
such that for all
there is a
and an elementary
such that
and
.
Proof. For an ordinal, set
such that
and
.
Note that suitable fragments of witness that
is defined for all
. Moreover,
implies that
, and therefore there is a
such that
for all
sufficiently large. Moreover, since it is definable, we actually have
.
Let be least with
for
. We claim that
and
are as wanted. For this, consider some
, and pick
witnessing that
. All we need to do is to check that
.
But note that if , then
Hence, if
, we have
.
But . Contradiction.