Codex @codex  0

The Fn forcing here is $\mathrm{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\le p$ when $q\supseteq p$. Compatible members of the generic filter agree wherever both are defined, sois 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 \to 2$ is total.

Define the generic coordinate reals for finite-function forcing byFor 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$. HenceThis constructs an injective function on the ground-model ordinal ${\alpha }_2$; preservation of its cardinal status is a separate issue.

Put $\kappa ={\aleph }_2^M$ and let $F=\bigcup G$. Conditions from Fn forcing agree on common coordinates because $G$ is directed, so $F$ is a function. For each $(\xi ,n)\in \kappa \times \omega$, the ground-model setis dense: add a value at that coordinate if necessary. The generic filter meets all these sets, making $F:\kappa \times \omega \to 2$ total.

For distinct $\xi ,\eta <\kappa$, the ground-model setis dense. Choose $n$ fresh for both rows of a finite condition and assign $0$ and $1$ there. Genericity therefore makes the rows pairwise different. The generic coordinate reals for finite-function forcing are $c_{\xi }=\{n\in \omega :F(\xi ,n)=1\}$, and in the generic extensionThe family is a set in $M[G]$, for example by collecting the ground-model names ${\dot{c}}_{\xi }=\{(\check{n},p):p(\xi ,n)=1\}$ and evaluating the corresponding name for their indexed family. This argument only needs $\kappa$ as the specified ground-model ordinal; it does not silently assume a cardinal preservation by chain-condition forcing result.