Replacement in the Easton class extension

Fix $a={\tau }_G$, choose an infinite regular $\lambda$ above the stages of $\tau$ and $\vec{\rho }$ with $\mu :=\mid \mathrm{dom}(\tau ){\mid }^M<\lambda$, and enumerate $\mathrm{dom}(\tau )=⟨{\sigma }_{\alpha }:\alpha <\mu ⟩\in M$ [F4]; then $a\subseteq \{{\sigma }_{\alpha ,G}:\alpha <\mu \}$ and $a,{\vec{\rho }}_G\in M[G^{\le \lambda }]$ by the valuation and stage clauses of [F1]. Assume $M[G]\models \mathrm{\forall }x\in a\mathrm{\exists }!y\psi (x,y,{\vec{\rho }}_G)$. This assertion concerns only the active values ${\sigma }_{\alpha ,G}\in a$; a name in $\mathrm{dom}(\tau )$ whose coefficient is not met by $G$ may have a value outside $a$.

Apply [F2] to the formula $\mathrm{\exists }y\psi (x,y,\vec{\rho })$ and the tuples $({\sigma }_{\alpha },\vec{\rho })$, obtaining $t\in G^{>\lambda }$, maximal antichains $W_{\alpha }$ and, for every cell $q\in W_{\alpha }$ with a positive recorded value, a ground name ${\rho }_{\alpha ,q}$ with $t\cup q⊩\psi ({\sigma }_{\alpha },{\rho }_{\alpha ,q},\vec{\rho })$. Put $S=\{{\rho }_{\alpha ,q}:\alpha <\mu ,q\in W_{\alpha },\text{ the value recorded at }q\text{ is positive}\}$, a ground set indexed by the set $\mu \times {\bigcup }_{\alpha <\mu }{W}_{\alpha }$ [F3, F4]; by the last clause of [F2] there is an infinite regular $\gamma$ with $S\subseteq M^{P^{\le \gamma }}$, and then $\{{\rho }_G:\rho \in S\}=\{{\rho }_{G^{\le \gamma }}:\rho \in S\}\in M[G^{\le \gamma }]$ by [F1].

Every actual value lies in that image. Let $x={\sigma }_{\alpha ,G}\in a$ and let $y$ be the unique element of $M[G]$ with $M[G]\models \psi (x,y,{\vec{\rho }}_G)$. The truth value of the existential instance was decided on the antichain $W_{\alpha }$ by the unique $q_{\alpha }\in W_{\alpha }\cap G^{\le \lambda }$ from [F2]. Its recorded value cannot be negative: then a condition of $G$ extending $t\cup q_{\alpha }$ would force $\mathrm{\neg }\mathrm{\exists }y\psi ({\sigma }_{\alpha },y,\vec{\rho })$, contradicting soundness in the actual extension and the existence of $y$. Hence the positive cell carries ${\rho }_{\alpha ,q_{\alpha }}\in S$ and forces $\psi ({\sigma }_{\alpha },{\rho }_{\alpha ,q_{\alpha }},\vec{\rho })$. Soundness gives $M[G]\models \psi ({\sigma }_{\alpha ,G},{\rho }_{\alpha ,q_{\alpha },G},{\vec{\rho }}_G)$, so uniqueness yields $y={\rho }_{\alpha ,q_{\alpha },G}\in \{{\rho }_G:\rho \in S\}$. Thus the image is a subset of this set and is itself a set of $M[G]$ by Separation [F3].

Replacement follows since $\psi$, the parameters and $a$ were arbitrary, and the proof shows in addition that the image is contained in the value of a ground set of witness names all of which lie in the single stage $M^{P^{\le \gamma }}$: this is the statement. ∎