Kunen inconsistency theorem (source code)

= Kunen inconsistency theorem
{c}

In <ZFC> there is no nonidentity <elementary embedding> $j:V\to V$, understood as an ordinary class embedding whose set restrictions and critical sequence are available. Let $\lambda$ be the supremum of the <Kunen critical sequence>, so $j(\lambda)=\lambda$ and $j(\lambda^+)=\lambda^+$. Partition the ordinals of cofinality $\omega$ below $\lambda^+$ into stationary sets indexed by the critical point. After applying $j$, the extra stationary cell at that critical point meets the club of ordinals closed under $j$. Such an ordinal of countable cofinality is fixed by $j$ and hence belongs both to that extra cell and an old-index cell, a contradiction.