Kunen lemma

Let $j:V\to M$ be a nonidentity elementary embedding into a transitive class model of ZFC, with its set restrictions and Kunen critical sequence available. Let $\lambda ={\sup }_{n<\omega }{j}^n(\kappa )$ for $\kappa =\mathrm{crit}(j)$. Then $j(\lambda )=\lambda$ andThese domain and closure assumptions are essential; the assertion is not a statement about an arbitrary elementary map between arbitrary structures.^[ref]

For the combinatorial argument, choose an omega-Jónsson function $f:[\lambda {]}^{\omega }\to \lambda$: every subset of $\lambda$ of cardinality $\lambda$ has all $\lambda$ possible values on its countable subsets. If $X=j‘‘\lambda$ belonged to $M$, its order type would be $\lambda$, so $M$ would see it as a set of cardinality $\lambda$. Elementarity would make $j(f)$ take every value below $\lambda$ on its internally countable subsets. But every such subset $Y\subseteq X$ is $j(Z)$ for a countable $Z\subseteq \lambda$, since $j$ fixes countable enumerations coordinatewise. HenceThe value $\kappa$ is omitted by that image, a contradiction. The existence of omega-Jónsson functions is the combinatorial input; the rest tracks precisely what the target model could contain.