Schema of continuity in the basic Cohen model

If $m=0$, take the empty family of clopens: there is one empty tuple, and the conclusion is the given truth. Assume $m>0$. By the truth lemma choose $p^{\mathrm{\prime }}\in G$ which forces $\phi (\check{\stackrel{ˉ}{x}},\dot{s},\dot{A})$, where ${\dot{s}}_j={\dot{a}}_{h(j)}$. It is enough to show that below every such $p^{\mathrm{\prime }}$ there is a condition forcing the asserted clopen-box conclusion, because density closure and the truth lemma then put that conclusion in $V[G]$.

Extend $p^{\mathrm{\prime }}$ to a condition $p$ and choose $k\in \omega$ so that $\mathrm{dom}(p)=k\times k$, $\mathrm{rng}(h)\subseteq k$, and the rows $p_i=p\upharpoonright (\{i\}\times k)$ are pairwise distinct for $i<k$. This is a finite construction: first enlarge the rectangle, then give each pair of rows a fresh column on which their bits differ. Put $U_j=[p_{h(j)}]$. The $U_j$ are pairwise disjoint because their defining binary strings are incompatible, and $p$ forces ${\dot{a}}_{h(j)}\in U_j$.

Suppose, towards a contradiction, that some $r\le p$ forces that a tuple $\dot{t}\in {\dot{A}}^m$ lies in ${\prod }_{j<m}{U}_j$ but fails $\phi (\check{\stackrel{ˉ}{x}},\dot{t},\dot{A})$. By finitely many applications of the membership forcing clause and density, strengthen $r$ so that ${\dot{t}}_j={\dot{a}}_{z(j)}$ for a ground-model map $z:m\to \omega$. The disjointness of the $U_j$ and F2 make $z$ injective. Moreover, if $z(j)<k$, then $r\le p$ and $r⊩{\dot{a}}_{z(j)}\in [p_{h(j)}]$ give $p_{z(j)}=p_{h(j)}$; the pairwise distinct rows imply $z(j)=h(j)$. Thus every $z(j)\mathrm{\ne }h(j)$ lies outside $k$.

Let $\pi$ interchange $h(j)$ and $z(j)$ whenever they differ and fix every other coordinate. The transpositions are disjoint by the last conclusion of step 2.1. The symmetry lemma gives

A common extension of $p$ and $\pi r$ would force both $\phi (\check{\stackrel{ˉ}{x}},\dot{s},\dot{A})$, by persistence from $p\le p^{\mathrm{\prime }}$, and its negation, by step 3.1. This is impossible. Hence $p$ forces that every tuple from $A$ in the displayed clopen box satisfies $\phi$. Since such a $p$ is available below every $p^{\mathrm{\prime }}$ forcing the original instance, step 1.1 and density closure prove the first assertion in $V[G]$.

For the consequence, choose fixed formulas and ordinal parameters which uniquely define the finitely many supported parameters from $A,u$. Replace their occurrences in the desired assertion by those definitions and conjoin uniqueness. Apply the first assertion to the concatenated tuple $u^{⌢}s$. Keep the coordinates belonging to $u$ at their original values and retain only the clopens belonging to $s$. All clopens in the larger box are pairwise disjoint, so the retained ones avoid $\mathrm{rng}(u)$; unique definability restores the fixed parameters after every permitted substitution. The construction is finite and makes no choice from an arbitrary family.