Countable chain condition for finite-function forcing (source code)

= Countable chain condition for finite-function forcing
{title2=$\operatorname{Fn}(X,Y,\omega)\text{ is ccc for countable }Y$}

The order $\operatorname{Fn}(X,Y,\omega)$ has the <countable chain condition for forcing> whenever $Y$ is countable. For an uncountable family of conditions, apply the <Delta-system lemma> to the finite domains. On their common finite root there are only countably many assignments, so thin to an uncountable family agreeing on that root. Any two conditions now have a compatible union. For binary <Cohen forcing>, there are only finitely many root assignments.