Cohen-name valuation and dense-set meeting

Two conditions in G have a common extension and hence agree on the intersection of their domains. Thus their union c is a binary partial function. For each n, $D_n=\{s:\mathrm{length}(s)>n\}$ is a dense set in M: extend any short sequence with zeros to length n+1. Genericity supplies a condition of G of length above n, so the domain of c is all omega.

For each binary sequence $r\in M$, the set $E_r=\{s:\mathrm{\exists }n<\mathrm{length}(s)s(n)\mathrm{\ne }r(n)\}$ belongs to M and is dense. Given s, if it already disagrees it is in E_r; otherwise append the bit $1-r(\mathrm{length}(s))$. A condition of $G\cap E_r$ witnesses $c\mathrm{\ne }r$.

Internal Replacement and Union over the set of finite sequences and their finitely many coordinates form tau in M. Every entry has a name as its first coordinate, so tau is a name. F1 makes its value exactly $\{⟨n,s(n)⟩:s\in G,n<\mathrm{length}(s)\}$, the graph of c by step 1.1. Each graph coordinate is included by a condition covering n, and any selected entry agrees with c.