Jech–Sochor first embedding theorem

Work first in $M$. By [F5], the choices stated above can be made with $A^{\mathrm{\prime }}$ a pure ordinal and a bijection $j:A\to A^{\mathrm{\prime }}$. The ordinal $\kappa$ and the set $A^{\mathrm{\prime }}$ belong to $K$; regularity of $\kappa$ in $M$ implies regularity in $K$, since any shorter cofinal sequence in $K$ would also belong to $M$. By [F4], $K$ satisfies ZFC. Work in the specified $K$-generic outer universe for the poset $P\in K$ of partial binary functions of size $<\kappa$ on $(A^{\mathrm{\prime }}\times \kappa )\times \kappa$. The pure coordinate set ensures that $P$, unlike a poset indexed directly by atoms, belongs to $K$; regularity makes it $<\kappa$-closed. Moreover, every $M$-set sequence of pure conditions and every $M$-set of pure conditions is itself pure and therefore belongs to $K$; closure and genericity apply to the ambient enumerations used below. For each $(a,\xi )$, use the coordinate $(j(a),\xi )$ to name a generic subset $x_{a\xi }$ of $\kappa$, put $a^{\ast }=\{x_{a\xi }:\xi <\kappa \}$, and $A^{\ast }=\{a^{\ast }:a\in A\}$. Recursively translate atoms to $a^{\ast }$ and sets to the set of translations of their members.

Transport each original atom permutation through $j$ to the blocks $\{j(a)\}\times \kappa$ of the pure coordinate set, allowing arbitrary within-block permutations. Generate a normal filter from the transported original filter and finite pointwise stabilizers. The coordinate names, each $a^{\ast }$, and $A^{\ast }$ are hereditarily symmetric. For the transported automorphism $\pi$, the atomic forcing clauses commute with $p\mapsto \pi p$ and $\dot{x}\mapsto \pi \dot{x}$: a common strengthening or subname witness is carried bijectively to one on the other side. Simultaneous induction on name ranks and then on formula complexity (including the existential name witness) gives $p⊩\phi (\vec{\tau })$ iff $\pi p⊩\phi (\pi \vec{\tau })$. This derives the equivariance used below from F2's definable forcing clauses, without assuming it as an extra theorem. A further simultaneous induction on rank proves $x\in y$ iff $x^{\ast }\in y^{\ast }$ and $x=y$ iff $x^{\ast }=y^{\ast }$; distinct coordinate generics make the atom case injective.

The translation of $x$ is hereditarily symmetric exactly when $x\in V$. For the reverse implication, take a least-rank counterexample and a symmetric name forced equal to its translation. A permutation from the original support filter moving $x$ can be lifted so that it fixes the finite coordinate support and moves the forcing condition to a compatible one, producing contradictory forced equalities.

Let $W$ be the interpretations of the hereditarily symmetric (HS) names for the lifted group and filter. These values are transitive and contain every pure check name. We establish almost universality relative to $K[G]$ without choosing simultaneous HS representatives. If an ambient set $x\in K[G]$ has $x\subseteq W$, take a $K$-name $\dot{x}$ for it. For each $(\tau ,p)\in \mathrm{dom}(\dot{x})\times P$, let $r(\tau ,p)$ be the least rank of an HS name $\sigma$ such that $p⊩\tau =\sigma$, or $0$ if none exists. The forcing relation and HS predicate are definable in $K$; Replacement there bounds these ranks by one ordinal $\gamma$. For $u\in x$, choose one pair $(\tau ,p)\in \dot{x}$ with $p\in G$ and ${\tau }_G=u$, and one HS name $\sigma$ evaluating to $u$. The truth lemma yields a common $q\in G$ below $p$ forcing $\tau =\sigma$; hence $r(\tau ,q)<\gamma$ and $u$ has an HS name below $\gamma$.

For $a,\vec{w}\in W$ and any bounded formula $\phi (u,\vec{w})$, use HS names $\dot{a},\dot{\vec{w}}$ and the subname $\{(\tau ,p)\in \mathrm{dom}(\dot{a})\times P:p⊩\tau \in \dot{a}\wedge \phi (\tau ,\dot{\vec{w}})\}$. Its immediate subnames are HS; forcing equivariance makes the finite intersection of the parameter stabilizers fix it. Bounded absoluteness between the transitive $W$ and $K[G]$, followed by the truth lemma, identifies its value with the desired cut of $a$. Thus $W$ has ${\mathrm{\Delta }}_0$-Separation.

Let $S$ be the ground set of all HS names of rank below $\gamma$ and form the value-collecting name $\dot{y}=\{⟨\sigma ,p⟩:\sigma \in S\text{ and }p\in P\}$.

Its value is $\{{\sigma }_G:\sigma \in S\}$ because $G$ is nonempty. Automorphisms preserve $S$ and all of $P$, so $\dot{y}$ is fixed; its immediate subnames are HS. Thus $\dot{y}$ is itself HS and its value is a $W$-set containing $x$.

Now apply Jech's transitive-class criterion inside the ambient transitive ZF model $K[G]$. For $W$-parameters, each of its eight Gödel-operation outputs—unordered pair, difference, product, domain, the membership relation restricted to a square, and the three permutations of triple coordinates—is an ambient set whose members already lie in $W$: construct unordered and Kuratowski pairs first, then the remaining outputs in that order. Almost universality puts each output inside a $W$-set, and its bounded defining formula cuts it out by step 3.3. Hence $W$ is closed under all eight operations. Jech's formula-complexity induction from transitivity, almost universality, and this closure supplies full Comprehension, including unbounded quantifiers; the criterion also yields Pairing, Union, internal Power Set, Infinity, and Replacement. Thus $W$ is a symmetric ZF model between the kernel and the full generic extension. This argument uses no AC in $W$.

Induct through $\beta \le \alpha$ to prove surjectivity onto ${\mathcal{P}}^{\beta }(A^{\ast }{)}^W$. At $\beta =0$ this is the explicit bijection $a\mapsto a^{\ast }$ from step 2.1. At a limit $\beta$, both power-set hierarchies are the unions of their lower stages, so the compatible earlier identifications give the result. At a successor stage, the earlier members retain their translations. Put $x={\mathcal{P}}^{\beta -1}(A{)}^V$, and let $y={\dot{y}}_G\in W$ be a subset of the translated image $x^{\ast }$. By the truth lemma choose $p_0\in G$ forcing $\dot{y}\subseteq {\dot{x}}^{\ast }$. The ambient $M$-cardinality bound $\mathrm{\mid }x\mathrm{\mid }<\kappa$ from step 1.1 supplies an enumeration $⟨x_i:i<\lambda ⟩$ with $\lambda <\kappa$. Its translated pure-name sequence, together with $\dot{y}$, is a $K$-set by step 1.1. For each $i<\lambda$ the conditions deciding ${\dot{x}}_i^{\ast }\in \dot{y}$ are dense. Starting below any $p\le p_0$, recursively choose one stronger decider for each $i$ and take a lower bound at limit stages below $\lambda$, using $<\kappa$-closure. This pure recursion lies in $K$, so the set $D$ of conditions below $p_0$ deciding every listed membership is a $K$-dense set below $p_0$. Since $G$ is $K$-generic and contains $p_0$, choose $q\in G\cap D$. Define in $M$ the ground subset $z=\{x_i:i<\lambda ,q⊩{\dot{x}}_i^{\ast }\in \dot{y}\}$. The decisions and $q⊩\dot{y}\subseteq {\dot{x}}^{\ast }$ give $q⊩{\dot{z}}^{\ast }=\dot{y}$; in particular $z^{\ast }=y$ in the chosen generic extension. By the reverse HS criterion of step 3.1, the symmetric name $\dot{y}$ forced equal to the translation below $q$ implies $z\in V$. The dense-set/genericity step is essential: a lower bound deciding all memberships outside $G$ would not determine the actual $y$. Thus translation is a membership isomorphism at every lower iterate. If $A=\mathrm{\varnothing }$, the coordinate forcing is trivial and $W=K$, so the same identification includes the empty-atom endpoint. Ambient AC in $M$ supplies the well-order of ${\mathcal{P}}^{\alpha }(A)$, the regular cardinal $\kappa$, and the atom-to-pure-coordinate bijection; the pure kernel inherits AC for the closure recursion, while $W$ need not satisfy AC.