Finite-condition Lévy collapse (source code)

= Finite-condition Lévy collapse
{c}
{title2=$\operatorname{Lv}(\kappa)$}

The finite-condition Lévy collapse $\operatorname{Lv}(\kappa)$ consists of finite <partial functions> $p$ with $\operatorname{dom}p\subseteq\kappa\times\omega$ and $p(\alpha,n)<\alpha$, ordered by reverse inclusion. The generic union gives a surjection $\omega\to\alpha$ for every infinite $\alpha<\kappa$. If $\kappa$ is regular and uncountable, the <Delta-system lemma at a regular uncountable cardinal> proves the $\kappa$-chain condition, so the extension makes $\kappa=\aleph_1$.