The inaccessible Lévy-collapse setup for Solovay's construction

Let $U$ be a transitive model of ZFC and let $\kappa$ be strongly inaccessible in $U$. For the real--ordinal definability form of the Solovay model, take the forcing ground to be $V=L^U$. The constructible-inner-model theorem gives $V\models \mathrm{Z}\mathrm{F}\mathrm{C}+V=L$ with the same ordinals as $U$. Moreover, $\kappa$ is still inaccessible in $V$: regularity is downward absolute; $\kappa$ and unboundedly many $U$-cardinals below it remain cardinals in the inner model; and GCH in $V$ makes this regular limit cardinal a strong limit. The canonical setlike global well-order of $L$ also makes every ground-model parameter definable from an ordinal. We henceforth write $V$ for this constructible ground.

In $V$, let

$P=\mathrm{Lv}(\kappa )=\{p:p\text{ is a finite function},\mathrm{dom}(p)\subseteq \kappa \times \omega ,p(\alpha ,n)<\alpha \}\mathrm{.}$

ordered by reverse inclusion. This is the finite-condition presentation of $\mathrm{Coll}(\omega ,<\kappa )$. For $\xi <\kappa$, put $P_{\xi }=\{p\in P:\mathrm{dom}(p)\subseteq \xi \times \omega \}$ and, for a supplied $V$-generic filter $G\subseteq P$, put $G_{\xi }=G\cap P_{\xi }$.

The restriction map $p\mapsto p\upharpoonright (\xi \times \omega )$ is a complete projection: if $q\le p\upharpoonright (\xi \times \omega )$, then $q\cup (p\upharpoonright ((\kappa \setminus \xi )\times \omega ))\le p$ projects to $q$, since the initial and tail domains are disjoint. Thus $G_{\xi }$ is $P_{\xi }$-generic over $V$, $V[G_{\xi }]\subseteq V[G]$, and the remaining forcing is the quotient $P\mathrm{/}{G}_{\xi }$.

No model or generic is asserted to exist. Passing to $L^U$ adds no consistency hypothesis beyond the inaccessible in $U$. Choice is a ground/ambient hypothesis: it supports the usual cardinal comparisons, maximal-antichain arguments and forcing recursion. It is not included in the eventual inner model.