Kunen lemma (source code)

= Kunen lemma
{c}

For an elementary embedding with critical-sequence supremum $\widehat\kappa$, the set
$$
j\mathbin{``}\widehat\kappa=\{j(\xi):\xi<\widehat\kappa\}
$$
does not belong to the transitive target model. The proof uses an omega-Jonsson function on $\widehat\kappa$.