Finite reflection along constructible levels

Use $W_{\gamma }=L_{\gamma }$ and $W=L$. The recursive definition supplies uniform definability, the limit definition supplies continuity, and F1 supplies monotonicity and nonemptiness. Every element of $W$ belongs to a level by definition. These are precisely the general-class hypotheses of F2.

Apply the construction in F2 to the finite subformula closure of $\mathrm{\Phi }$, starting above $\alpha$ and above zero. It bounds the least witness stages for tuples in each set level using ambient Replacement, iterates that definable bound through omega, and takes the supremum $\beta$. Strict increase makes $\beta$ a nonzero limit. Each finite tuple lies in a stage of this sequence, so every true existential in the closed family has a witness before $\beta$; the witness criterion in F2 gives agreement in both directions. All these are ambient ZF operations, and no internal Replacement or satisfaction predicate for the whole class L is presumed.