Uniform head-antichain decisions below a class tail

For each $\alpha <\mu$ the class of conditions deciding $\phi ({\vec{\tau }}_{\alpha })$ is definable and dense by [F3] and [F5]. For a fixed $\alpha$ we build a good tail condition below any given $t_0\in P^{>\lambda }$: at successor stages choose a head condition incompatible with all previously chosen ones, strengthen the head and tail to decide $\phi ({\vec{\tau }}_{\alpha })$, and use the resulting stronger head condition as $q_{\xi }$. If $\phi$ is an outer existential formula and the decision is positive, strengthen head and tail once more and choose a ground witness name forcing its matrix by the existential density clause [F4]; the final head condition remains incompatible with earlier cells. Use the Global Choice least witness among those of least rank at each successor stage. At limit stages $\xi <{\lambda }^{+}$ take the union of the earlier tails, which is a condition by [F2]; class Replacement collects each set-length initial segment. If the construction did not stop before ${\lambda }^{+}$, class Replacement would collect a forbidden ${\lambda }^{+}$-sized head antichain. Decisions and attached witnesses persist under stronger tails. By the ${\lambda }^{+}$-chain condition of the head, this recursion must stop before ${\lambda }^{+}$, when the head antichain is maximal. The resulting tail is good for $\alpha$, so the class of tails good for one $\alpha$ is dense and open in $P^{>\lambda }$ and belongs to $\mathcal{C}$ by [F1]; the set-indexed choices and antichains are supplied by Global Choice and class Replacement in [F1] and ground Choice [F7].

Iterating step 1.1 along the $\alpha <\mu \le \lambda$ many indices: given $t$ good for all $\beta <\alpha$, apply step 1.1 to $t$ and $\alpha$ to get $t^{\mathrm{\prime }}\le t$ good for $\alpha$, and the antichains and decisions already attached to the earlier indices persist because decisions are inherited by stronger conditions by [F5], using monotonicity and the fact that $W_{\beta }$ remains maximal. Choose at each stage the least-rank witness tuple and then its Global Choice least representative; class Replacement [F1] collects the $\mu$-indexed antichains, decision maps and attached witness names into one ground set. Thus the class $D$ of tail conditions deciding $\phi$ on $⟨{\vec{\tau }}_{\alpha }⟩$ is the intersection of the $\mu$ many open dense classes, it is open and in $\mathcal{C}$, and it is dense in $P^{>\lambda }$: given $t_0$, build a descending sequence $⟨t_{\alpha }:\alpha <\mu ⟩$ with $t_{\alpha }$ good for all $\beta \le \alpha$ by recursion of length $\mu \le \lambda$, taking lower bounds at limits by ${\lambda }^{+}$-closure, and a lower bound of the whole sequence is in $D$ by openness.

The class $D^{\ast }=\{p\in P:p^{>\lambda }\in D\}$ is dense in $P$ and lies in $\mathcal{C}$, because below any $p$ the class $D$ supplies a tail condition $t\le p^{>\lambda }$ and then $p^{\le \lambda }\cup t\le p$ has its tail in $D$; so by the genericity of $G$ there is $t=p^{>\lambda }\in G^{>\lambda }$ with $t\in D$, and by [F6] $G^{>\lambda }$ is a directed filter in the tail.

Confirmation and definability in the head stage. Fix $t\in G^{>\lambda }\cap D$ from step 3.1 and $\alpha <\mu$. The antichain $W_{\alpha }$ and the decisions are ground sets, hence lie in $M[G^{\le \lambda }]$; since $G^{\le \lambda }$ is an $M$-generic filter on $P^{\le \lambda }$ [F6] and $W_{\alpha }$ is a maximal antichain of $P^{\le \lambda }$, there is exactly one $q_{\alpha }\in W_{\alpha }\cap G^{\le \lambda }$, and uniqueness uses directedness of the filter and pairwise incompatibility inside the antichain. The condition $t\cup q_{\alpha }$ is extended by an element of $G$: any common extension of $t$ and $q_{\alpha }$ in $G$ is below it, so by [F3] and [F5] the truth value of $\phi ({\vec{\tau }}_{\alpha ,G})$ in $M[G]$ is exactly the value recorded at $q_{\alpha }$, and the recorded value is a formula of $M[G^{\le \lambda }]$ with the ground parameters $W_{\alpha }$ and the decision function; consequently the set $\{\alpha <\mu :M[G]\models \phi ({\vec{\tau }}_{\alpha ,G})\}$ is defined in $M[G^{\le \lambda }]$ by Separation in that ZFC set extension [F7] applied to $\mu$. For an outer existential formula, its positive cells carry the witness names selected in step 1.1.

The witness names. The witnesses attached in step 4.1 are names of $M$ and they are indexed by the set $\mu \times {\bigcup }_{\alpha <\mu }{W}_{\alpha }$, which is a set of $M$ because each $W_{\alpha }$ is a set of cardinality at most $\lambda$ by [F2] and $\mu \le \lambda$; by Replacement in $M$ [F1] the class function sending each such name to the least infinite regular cardinal of its stage is bounded on this set, so there is an infinite regular $\gamma$ with $S\subseteq M^{P^{\le \gamma }}$; then $\{{\sigma }_G:\sigma \in S\}=\{{\sigma }_{G^{\le \gamma }}:\sigma \in S\}\in M[G^{\le \gamma }]$ by the stage valuation of [F3] and Replacement in the set extension [F7], which is the last clause.

Steps 2.1, 3.1, 4.1 and 5.1 establish (a), (b) and (c): a class-generic extension contains one tail condition and ground head antichains deciding the formula on every tuple, the truth values are computed in the head stage, and the witness names lie in one ground stage; this is the statement. ∎