The Feferman–Levy collapse argument is finitely formalizable

Expand the proofs of the finitely many formulas in $\mathrm{\Delta }$. For the three extra sentences, expand F1 and every dependency used in its collapse, Boolean-value, cardinal, cofinality, and truth-lemma arguments. For each ZF formula in $\mathrm{\Delta }$, expand only the corresponding instance of F3's HS verification. Every displayed proof is finite and every schema occurrence has one fixed formula, so this traversal produces a finite list $\mathrm{\Gamma }$ of ground ZFC+GCH axioms and schema instances.

Include in $\mathrm{\Gamma }$ the finite definitions and absoluteness instances for the collapse order, automorphism action, normal filter, Boolean completion, name ranks, forcing relation, HS predicate, and evaluation that actually occur in step 1.1. Include also the finitely many Separation and Replacement instances used to collect the bounded layers and the selected $\mathrm{\Delta }$-axioms. This is a finite syntactic union; rank recursion contributes its one fixed formula instance, not one axiom for every rank.

Apply F2 to this fixed source fragment and forcing specification. In ambient ZFC+GCH obtain a countable transitive set $M\models \mathrm{\Gamma }$ containing the required parameters and an $M$-generic $G$. Inside the set extension $M[G]$, form the interpretations of the HS names from $M$. Since $M$ is a set, their interpretations form an externally bounded set $N_M\subseteq M[G]$. The retained instances from steps 1.1–2.1 prove that $N_M$ satisfies every ZF formula in $\mathrm{\Delta }$ and all three extra sentences.

The quantifier over $\mathrm{\Delta }$ is external: for each one fixed finite list, the preceding finite trace supplies its corresponding $\mathrm{\Gamma }$ and proof. If the ZF part of $\mathrm{\Delta }$ is empty, the same construction still gives the three explicit sentences in a nonempty set model. Nothing here asserts a single model of full ZFC, a countable transitive model of full ZF, or a uniform truth predicate. Ambient AC is used only through F2 as recorded by F4; the constructed target satisfies the negative choice sentence.