Every set is countable in the intermediate extension

Fix an infinite regular ground cardinal $\delta$. The union $g_{\delta }=\bigcup \{p(\delta ):(p,U)\in G,\delta \in {\mathrm{dom}}_1(p)\}$ is a well-defined one-to-one partial map $\omega \to \delta$: two generic conditions have a common refinement, whose section extends both finite sections. For each $n<\omega$, support extension followed by finitely many legal successors gives a condition filling the $n$th slot, so the corresponding class is dense and $\mathrm{dom}(g_{\delta })=\omega$. For each $\xi <\delta$, every successor set in the coordinate filter is unbounded—co-bounded in the small case and of cardinality $\delta$ by uniformity in the ultrafilter cases—so pruning it above $\xi$ and taking the next successor is dense. Hence $\mathrm{ran}(g_{\delta })$ is cofinal in $\delta$. It is not claimed to equal $\delta$.

Let $\lambda$ be a nonzero limit ordinal and compute $\delta ={\mathrm{cf}}^M(\lambda )$. By F3, choose in $M$ an increasing cofinal $h:\delta \to \lambda$, and by F4 the ground cardinal $\delta$ is regular and infinite. If $\delta =\omega$, $h$ already witnesses countable cofinality in $M[G]$. If $\delta >\omega$, step 1.1 gives a cofinal $g_{\delta }:\omega \to \delta$, so $h\circ g_{\delta }$ has cofinal range in $\lambda$. A finite map cannot be cofinal in a nonzero limit ordinal, and therefore $M[G]\models \mathrm{cf}(\lambda )=\omega$.

Apply transfinite induction to “$\alpha$ is at most countable in $M[G]$.” The zero ordinal is finite. If $\alpha$ is countable, then $\alpha +1$ is countable by adjoining one point to a finite or $\omega$-enumeration. At a nonzero limit $\lambda$, choose the cofinal map $c:\omega \to \lambda$ from step 2.1. Every $c(n)+1<\lambda$ is countable by the induction hypothesis, and $\lambda ={\bigcup }_{n<\omega }(c(n)+1)$. The definable global well-order from F2 supplies ${\mathrm{A}\mathrm{C}}_{\omega }$, so F6 makes this union countable. F5 now gives that every ordinal of $M[G]$ is at most countable.

Let $x\in M[G]$. If $x=\mathrm{\varnothing }$, F8 makes it finite and countable. Otherwise the definable global well-order from F2 restricts to a well-order of $x$; Replacement supplies its ordinal order type $\alpha$ and a bijection $x\cong \alpha$. Step 3.1 makes $\alpha$, and hence $x$, at most countable. By F7 this is equivalent, in the nonempty case only, to a surjection $\omega \to x$.