Two-step forcing iterations

Let $P$ be a set-sized forcing preorder with largest condition and let $\dot{Q}$ be a $P$-name such that $1_P⊩\dot{Q}$ is a nonempty forcing preorder with largest condition. Put $S_0=\mathrm{dom}(\dot{Q})$, where the domain is the set of names occurring as first coordinates in $\dot{Q}$, and recursively put $S_{n+1}=S_n\cup {\bigcup }_{\sigma \in S_n}\mathrm{dom}(\sigma ),U={\bigcup }_{n<\omega }{S}_n\mathrm{.}$ Thus $U$ contains every immediate subname of each $\sigma \in \mathrm{dom}(\dot{Q})$ and is closed under immediate subnames. It is a set of $P$-names in the ground model. Let $R$ be the set of all $P$-names $\rho \subseteq U\times P$; Power Set and Separation make $R$ a set, without Choice. The two-step iteration $P\ast \dot{Q}$ is the set of pairs $(p,\dot{q})\in P\times R$ such that $p⊩\dot{q}\in \dot{Q}$, ordered by

$(p,\dot{q})\le (p^{\mathrm{\prime }},{\dot{q}}^{\mathrm{\prime }})⟺p{\le }_P{p}^{\mathrm{\prime }}\text{ and }p⊩\dot{q}{\le }_{\dot{Q}}{\dot{q}}^{\mathrm{\prime }}\mathrm{.}$

Names forced equal below $p$ represent equivalent second coordinates at $p$; substitution into the displayed order is valid because forcing respects equality. Reflexivity and transitivity follow from the forced preorder axioms.

Under AC, this set-sized convention represents every condition in the unrestricted local-name convention. If $p⊩\dot{\tau }\in \dot{Q}$, then below $p$ it is dense to force $\dot{\tau }=\sigma$ for some $\sigma \in \mathrm{dom}(\dot{Q})$, by the forcing membership clause. Choose a maximal antichain $C$ below $p$ inside that dense set and, for each $c\in C$, one such ${\sigma }_c$. Mix the ${\sigma }_c$ along $C$: retain a pair $(\nu ,s)$ whenever $(\nu ,t)\in {\sigma }_c$ for some $c\in C$ and $s\le c,t$. Every $\nu$ used is an immediate subname of a ${\sigma }_c$, so the mixed name $\rho$ lies in $R$. For each $c\in C$, $c⊩\rho ={\sigma }_c=\dot{\tau }$; predensity of $C$ below $p$ gives $p⊩\rho =\dot{\tau }$. Hence $(p,\rho )$ is equivalent to the original local condition, and the restricted iteration is dense/equivalent to that convention. The same construction at $p=1_P$ supplies a name in $R$ for the forced largest condition of $\dot{Q}$. The set carrier and order exist in ZF; the maximal-antichain and simultaneous-mixing claim here uses AC. This definition makes no generic-factorization or chain-condition assertion.