The intermediate extension satisfies ZF minus Power Set plus Collection

Every ground-definable antichain in $P_3$ is a set. Otherwise the ground global well-order recursively selects a proper-class sequence $⟨(p_{\xi },U_{\xi }):\xi \in \mathrm{Ord}⟩$ of distinct members. Thin first to a fixed finite support size and fixed finite pattern of section lengths. If every coordinate position were bounded, the antichain would lie in one set $P_{\theta }$, so some least support position is unbounded. All earlier positions are bounded by an ordinal $\beta$; thin so that the finite supports above $\beta$ are pairwise disjoint. There are only set many restrictions in $P_{{\beta }^{+}}$, so one proper subclass has identical bounded restriction. Any two conditions in that subclass now have compatible overlap and disjoint upper supports, and F2 amalgamates them, contradicting antichainhood.

Define $\mathrm{\Delta }(x)$ to be the least regular $\theta$ with $x\in M[G_{\theta }]$, and within that least stage choose the $W_O$-least $P_{\theta }$-name evaluating to $x$. These data lexicographically order $M[G]$. They are definable by F1 and use the supplied predicate from F3. To see that every nonempty set $a$ has a least member, choose $x_0\in a$; only regular stages at most $\mathrm{\Delta }(x_0)$ can improve its first coordinate, and those form a set. At the least occupied stage, the set-like restriction of $W_O$ chooses the least evaluating name. Hence the relation is a definable global well-order of $M[G]$.

Extensionality is absolute because $M[G]$ is transitive. Given finitely many parameters, F2 puts them in one $M[G_{\theta }]$, a transitive ZFC set-forcing extension; its empty set, pair, union and $\omega$ are unchanged in the larger union, proving Empty Set, Pairing, Union and Infinity. If $a\mathrm{\ne }\mathrm{\varnothing }$, put $a$ in one such stage and take there an $\in$-minimal member of $a$; transitivity makes it still $\in$-minimal in the full union, proving Foundation.

Every nonempty ground-definable class $C$ of conditions has a set-sized maximal antichain. Traverse the ground global well-order $W_O$ and accept the least member of $C$ incompatible with every previously accepted member. If this never became maximal, the accepted class would be a ground-definable proper-class antichain, contrary to step 1.1. The accepted set is therefore maximal among conditions compatible with some member of $C$; in particular, below any $c\in C$, common refinements with the antichain are dense.

Fix a formula $\phi (x,\vec{z})$ of the expanded language, a name $\tau$ for $a$, names for $\vec{z}$, and $p_0\in G$ forcing any hypotheses in use. For every occurrence $(\sigma ,p)\in \tau$, let $C_{\sigma ,p}$ be the definable class of common refinements of $p,p_0$ which force $\phi (\sigma ,\vec{z})$. If this class is nonempty, use step 2.1 to choose an antichain $A_{\sigma ,p}\subseteq C_{\sigma ,p}$ maximal among these positive conditions; otherwise put $A_{\sigma ,p}=\mathrm{\varnothing }$. Form the set name $\dot{b}=\{(\sigma ,q):(\sigma ,p)\in \tau ,q\in A_{\sigma ,p}\}$. If $x\in {\dot{b}}_G$, some $q\in G$ lies in a positive antichain, so $x\in a$ and F1 gives $\phi (x,\vec{z})$. Conversely, if $x\in a$ and $\phi (x,\vec{z})$, choose $(\sigma ,p)\in \tau$ with $p\in G$ and ${\sigma }_G=x$; F1 gives a positive condition in $G$ below $p,p_0$, and maximality makes common refinements with $A_{\sigma ,p}$ dense there, so genericity puts a member of $A_{\sigma ,p}$ in $G$. Thus $x\in {\dot{b}}_G$. This proves Separation. For $a=\mathrm{\varnothing }$, the constructed name is empty.

Suppose $p_0$ forces $\mathrm{\forall }x\in \tau \mathrm{\exists }y\phi (x,y,\vec{z})$. For each $(\sigma ,p)\in \tau$, consider the definable class of common refinements $q\le p,p_0$ equipped with a set name $\rho$ such that $q{⊩}_3\phi (\sigma ,\rho ,\vec{z})$. Whenever $p$ is compatible with $p_0$, this class projects densely below their common cone: such a $q$ forces $\sigma \in \tau$, so the forced premise and the dense named-witness clause F5, used in F1's fixed-formula class recursion, give a stronger named witness. By step 2.1 choose a set maximal antichain of projected conditions and, using $W_O$, the least witness name ${\rho }_q$ for each member. Ground Replacement over the set of occurrences in $\tau$ and these set antichains forms the set name $\dot{c}=\{({\rho }_q,q):q\text{ occurs in one of them}\}$. For every $x\in {\tau }_G$, directedness below the corresponding $p,p_0\in G$ and genericity meet its antichain, so some $({\rho }_q{)}_G\in {\dot{c}}_G$ witnesses $\phi (x,({\rho }_q{)}_G,\vec{z})$. This proves Collection, including the empty-domain case.

For a functional formula, Collection gives a set containing every unique value, and Separation cuts out exactly those values; hence Replacement follows. Together with step 1.3 and Separation this is ZF without Power Set. Neither the antichain construction nor the witness-name construction formed all subsets of any set: they used only ground Replacement and Separation on already available set names and antichains. Thus the omission of Power Set is genuine, while step 1.2 supplies the additional definable global well-order.