Saturated elementary extension theorem (source code)

= Saturated elementary extension theorem
{title2=$M\preccurlyeq N,\quad N\text{ is }\kappa\text{-saturated}$}

For every infinite regular <cardinal> $\kappa$, every <first-order structure> has a $\kappa$-saturated <elementary extension>. At one stage use the <compactness theorem> with the <elementary diagram> to realize all <complete types> over <subsets> of the stage having size less than $\kappa$. There is a <set> of such types; finite <subsets> of the enlarged theory are satisfiable because their finitely many witnesses are independent. Iterate for $\kappa$ stages, taking elementary <unions> at limits. Regularity puts any parameter <set> of size less than $\kappa$ inside one stage, and its type is realized at the next one. Passing to a larger <regular cardinal> covers singular requested degrees of saturation as well.