Separation and Power Set in the Easton class extension

Fix $a={\tau }_G\in M[G]$ with $\tau \in M^{P^{\le {\lambda }_0}}$ for an infinite regular ${\lambda }_0$ [F1]. Choose an infinite regular $\lambda \ge {\lambda }_0$ with $\mu :=\mid \mathrm{dom}(\tau ){\mid }^M<\lambda$, possible because the ground has arbitrarily large regular cardinals, and enumerate $\mathrm{dom}(\tau )=⟨{\sigma }_{\alpha }:\alpha <\mu ⟩\in M$ using [F6]. Let $I=\{\alpha <\mu :\mathrm{\exists }p\in G^{\le \lambda }(⟨{\sigma }_{\alpha },p⟩\in \tau )\}$. Since $\tau$ is a head name, the valuation clause of [F1] gives $a=\{{\sigma }_{\alpha ,G}:\alpha \in I\}$; the activity set $I$ and $a$ lie in $M[G^{\le \lambda }]$ by Separation and valuation there, and $\mu \le \lambda$.

Separation. Let $\psi (x,\vec{\rho })$ be a fixed formula with parameter names $\vec{\rho }$ naming elements of $M[G]$; enlarging $\lambda$ if necessary, we may assume the parameters also lie in $M^{P^{\le \lambda }}$ [F1]. Apply [F2] with the tuples $({\sigma }_{\alpha },\vec{\rho })$, $\alpha <\mu \le \lambda$, to get $t\in G^{>\lambda }$ and maximal antichains $W_{\alpha }$ with decisions; the decision data lie in $M[G^{\le \lambda }]$. For each $\alpha <\mu$ let $q_{\alpha }\in W_{\alpha }\cap G^{\le \lambda }$ be the unique member met by the generic head, and let $b=\{\alpha \in I:\text{the recorded decision at }{q}_{\alpha }\text{ is positive}\}$. The activity set $I$ is in the head stage by step 1.1, and the decision data and the enumeration $\alpha \mapsto {\sigma }_{\alpha ,G}$ are there too, so $b\subseteq \mu$ and $\{{\sigma }_{\alpha ,G}:\alpha \in b\}$ are sets of the ZFC head stage [F5]. By [F2] the recorded value is the truth value of $\psi ({\sigma }_{\alpha ,G},{\vec{\rho }}_G)$ in $M[G]$, and step 1.1 says the active $\alpha$ enumerate exactly $a$. Thus this set is $\{x\in a:M[G]\models \psi (x,{\vec{\rho }}_G)\}$, which proves Separation.

Power Set. Let $b\subseteq a$ with $b\in M[G]$. Choose an infinite regular $\gamma \ge \lambda$ with $b\in M[G^{\le \gamma }]$ [F1] and define the membership code $c(\alpha )=1$ if ${\sigma }_{\alpha ,G}\in b$ and $c(\alpha )=0$ otherwise, for $\alpha <\mu$; extend it to $\bar{c}:\lambda \to M$ by $\bar{c}(\alpha )=0$ for $\mu \le \alpha <\lambda$ and read $\bar{c}$ as a function into $\{0,1\}\subseteq M$. Both $c$ and $\bar{c}$ lie in $M[G^{\le \gamma }]$ because $b$ and the enumeration do. In the factorization $P^{\le \gamma }\cong P^{\le \lambda }\times P^{(\lambda ,\gamma ]}$ of [F5] the second factor is ${\lambda }^{+}$-closed by [F4] and the first is ${\lambda }^{+}$-cc by [F4], so [F3] gives $\bar{c}\in M[G^{\le \lambda }]$ and hence $c\in M[G^{\le \lambda }]$. Therefore $b=\{{\sigma }_{\alpha ,G}:c(\alpha )=1\}$ is a set of $M[G^{\le \lambda }]$ by Replacement there, again using [F5]. As $b\subseteq a$ was arbitrary, every subset of $a$ in $M[G]$ lies in $M[G^{\le \lambda }]$; since $a\in M[G^{\le \lambda }]$ by step 1.1 and $M[G]\supseteq M[G^{\le \lambda }]$, this says $\mathcal{P}(a{)}^{M[G]}=\mathcal{P}(a{)}^{M[G^{\le \lambda }]}\in M[G^{\le \lambda }]$, which is Power Set for $a$.

Steps 2.1 and 2.2 prove Separation and the bounded power-set clause for the arbitrary $a\in M[G]$; applying the clause with $a$ an ordinal of $M$ gives the subset clause, and since every set has its $M[G]$-power set inside some stage, Power Set holds in $M[G]$. This is the statement. ∎