# Replacement axiom and existence of end-extensions (Chang and Keisler's Model Theory)

I am currently reading Chang and Keisler's model theory textbook, and there is something that I don't seem to be able to understand about their proof (through the Omitting Types Theorem) that every countable model $\mathfrak A = \langle A, E\rangle$ of $ZF$ has an end-elementary extension $\mathfrak B = \langle B, F\rangle$ (Theorem 2.2.18 in the third edition of the book). The main argument is fine, but I don't understand the way in which they apply the axiom of replacement in their proof that a certain theory $T$ locally omits certain types. Here's the part I am having trouble with:

First, they note that a formula $\phi(x, c)$ is consistent with $T$ if and only if $$(\mathfrak A, a)_{a \in A} \models (\forall y)(\exists z)(\exists x)[z \not \in y \wedge \phi(x, z)].$$

Then they take an element $a \in A$ and a formula $\phi(x, c)$ (a candidate for locally realizing a certain type which we want to omit) and show that $\phi(x, c) \wedge x \in a$ must be consistent with $T$ - so far so good. Then they claim - and here's where I am stuck:

Using the axiom of replacement in ZF, we see in turn that the following sentences hold in $(\mathfrak A, a)_{a \in A}$: $$(\forall y)(\exists z)(\exists x)[z \not \in y \wedge \phi(x, z) \wedge x \in a]$$ $$(\exists x)(\forall y)(\exists z)[z \not \in y \wedge \phi(x, z) \wedge x \in a]$$

and from the second sentence they conclude that for some $b \in A$, $\phi(b, c) \wedge b \in a$ is consistent with $T$, and the theorem follows easily.

My problem is with the passage from the first sentence, which follows at once from $\phi(x, c) \wedge x \in a$ being consistent with $T$, to the second one, in which $x$ is the same for any choice of $y$. I take it that I have to apply the axiom of replacement here - but how? I can see how to use collection to obtain, from the first sentence, something like

$$(\exists u)(\forall y)(\exists z)(\exists x)[x \in u \wedge z \not \in y \wedge \phi(x,z) \wedge x \in a];$$

But that's not what the second sentence says, and it is not enough to conclude the proof.

Chances are that I am forgetting about something bloody obvious, but I've been thinking about this for a couple of days now and I just don't see it. Where is it that I am being stupid?

Thanks!

-
An alternative proof of the fact uses definable ultrapowers, rather than the omitting types theorem. One constructs a filter on $\text{Ord}^M$ measuring every definable (with parameterrs) class in $M$, such that every class function $f:\text{Ord}\to M$ in $M$ that is bounded on a set in the filter is constant on a set in the filter. The resulting $M$-ultrapower will be an elementary end-extension of $M$. –  Joel David Hamkins Jul 2 '13 at 19:23

The negation of the second formula is logically equivalent to $$\forall x\in a\,\exists y\,\forall z\,(\phi(x,z)\to z\in y).$$ Using collection (and union), this implies $$\exists y\,\forall x\in a\,\forall z\,(\phi(x,z)\to z\in y),$$ which is equivalent to the negation of the first formula.