Small sets of ground ordinals are captured at a bounded iteration stage

Work in the given extension $V[G]$. By F2 choose a ground cardinal $\nu <\mathrm{cf}(\delta )$ equal to $\mathrm{\mid }A\mathrm{\mid }$ there, and choose in $V[G]$ a surjection $f:\nu \twoheadrightarrow A$. The truth lemma gives a ground $P_{\delta }$-name $\dot{f}$ and $p\in G$ forcing that $\dot{f}:\check{\nu }\to \mathrm{Ord}$ and is onto a name $\dot{A}$ for $A$. Thus the antichains below are indexed by the ground ordinal $\nu$, not by the extension set $A$. For every $\xi <\nu$, choose in the ground model a maximal antichain below $p$ deciding $\dot{f}(\check{\xi })$ as some check ordinal. Each antichain is countable by ccc. There are fewer than $\mathrm{cf}(\delta )$ antichains, and every condition has finite support, so the union $S$ of all their supports, together with $\mathrm{supp}(p)$, has size below $\mathrm{cf}(\delta )$. AC supplies the simultaneous antichains and code.

By regularity of $\mathrm{cf}(\delta )$, $S$ is bounded by some $\alpha <\delta$. Normalize $p$ and every member $a$ of every chosen antichain: replace each coordinate outside its finite support by the distinguished literal top name. At such a coordinate the original prefix forces equality to top, so induction on coordinates makes the normalized condition forcing-equivalent to the original in both order directions and preserves every decision. The normalized support is still contained in $\alpha$; hence these conditions, unlike the raw ones, are literal top-paddings of their $P_{\alpha }$ restrictions. Replace each antichain by its normalized image, removing duplicates if needed. Equivalence preserves antichain maximality below normalized $p$ and the ordinal labels.

Each normalized antichain is predense below normalized $p\mathrm{\mid }\alpha$ in $P_{\alpha }$: a $P_{\alpha }$-extension of that prefix has a top-padding below normalized $p$; maximality supplies a compatible normalized antichain member, and F3 reflects compatibility between these padded conditions. For each $\xi <\nu$, label the resulting $P_{\alpha }$-antichain by the ground ordinal it forces for $\dot{f}(\check{\xi })$. These labelled antichains define an explicit $P_{\alpha }$-name ${\dot{f}}_{\alpha }$; this construction does not restrict the original $P_{\delta }$-name $\dot{f}$. Since normalized $p$ is equivalent to $p\in G$, it belongs to $G$, and $G_{\alpha }$ meets each predense antichain below its prefix. The corresponding padded antichain member lies in $G$ and forces the same value of $\dot{f}(\check{\xi })$, so ${\dot{f}}_{\alpha ,G_{\alpha }}=f_G$. Thus its range $A$ lies in $V[G_{\alpha }]$. F2 ensures that “fewer than $\mathrm{cf}(\delta )$” has not changed.

A structure or indexed family coded by a small set of ground ordinals is recovered by fixed decoding operations from that set, so it belongs to the same intermediate model. The coding qualification is essential: no assertion is made for arbitrary unbounded collections lacking such a code.