The Easton class-generic union satisfies ZFC

Transitivity and ordinals. If $u\in {\tau }_G\in M[G]$, then $u={\sigma }_G$ for some pair $⟨\sigma ,p⟩\in \tau$ by the valuation clause of [F1], so $u\in M[G]$ and $M[G]$ is transitive; and every $x\in M$ equals its check-name value in $M[G]$ by [F5], so $M\subseteq M[G]$. Each stage has exactly the ordinals of $M$ by [F4], and the stages are nested by [F1], so the ordinals of $M[G]$ are exactly those of $M$.

The easy axioms. Extensionality and Foundation are inherited from the ambient universe because $M[G]$ is transitive and its membership relation is the true one; Infinity holds because $\omega \in M\subseteq M[G]$ by step 1.1. For Pairing and Union, given $x_1,\dots ,x_n\in M[G]$, choose by [F1] a single stage $M[G^{\le \lambda }]$ containing all of them, possible because the stages are nested and every element lies in some stage; then $\{x_1,\dots ,x_n\}$ and $\bigcup x_1$ are elements of that ZFC model by [F4] and hence of $M[G]$. Choice holds because each stage satisfies it by [F4] and [F6], so every element of $M[G]$ carries a well-ordering in $M[G]$, and the well-orderable sets of an extension form a model of Choice.

The hard axioms. Separation is [F2], Replacement is [F3], and Power Set with the bounded clause is [F2] as well; together with step 2.1 and step 1.1 this makes $M[G]$ a transitive model of ZFC containing $M$ with the same ordinals and the truth lemma of [F1]. Applying the bounded power-set clause of [F2] to the ordinal $a=\lambda \in M\subseteq M[G]$ gives an infinite regular $\gamma$ with $\mathcal{P}(\lambda {)}^{M[G]}=\mathcal{P}(\lambda {)}^{M[G^{\le \gamma }]}\in M[G^{\le \gamma }]$, which is the last clause.

Steps 1.1, 2.1 and 3.1 establish every clause: $M[G]$ is a transitive ZFC model containing $M$ with the ordinals of $M$, carries the definable class forcing relation and its truth lemma, and has all subsets of any ground ordinal inside one set stage. This is the statement. ∎