= Solution
The <Fn forcing> here is $\operatorname{Fn}(\alpha_2\times\omega,2,\omega)$; larger partial functions are stronger conditions. This translates the inclusion description into <standard notation for forcing> as $q\leq p$ when $q\supseteq p$. Compatible members of the <generic filter> agree wherever both are defined, so
$$
F=\bigcup G
$$
is a function. For every $(\xi,n)\in\alpha_2\times\omega$, the conditions whose domains contain that coordinate form a <dense subset of a forcing order>. This requirement belongs to $M$, and the <generic filter> meets it. Consequently $F:\alpha_2\times\omega\to2$ is total.
Define the <generic coordinate reals for finite-function forcing> by
$$
a_\xi=\{n<\omega:F(\xi,n)=1\}.
$$
For distinct $\xi,\eta<\alpha_2$, the conditions assigning opposite bits to those rows at some column form a <dense subset of a forcing order>. Given any finite condition, choose a column absent from both rows and extend by assigning zero to one coordinate and one to the other. Genericity supplies such a condition in $G$, so $a_\xi\ne a_\eta$.
The function $\xi\mapsto a_\xi$ is formed inside $M[G]$ by separation and replacement from $F$. Hence
$$
\boxed{M[G]\models\text{“}\xi\mapsto a_\xi\text{ is an injection }\alpha_2\to\mathcal P(\omega)\text{”}}.
$$
This constructs an <injective function> on the ground-model ordinal $\alpha_2$; preservation of its cardinal status is a separate issue.
Back to article page
