# What's the idea behind the proof of saturation of internal sets via ultrapower construction?

I'm trying to understand the proof of saturation of internal sets via ultrapower construction on Robert Goldblatt's Lectures on the Hyperreals: An Introduction to Nonstandard Analysis. Though, it's not a lengthy proof, I find it difficult to grok the idea behind the proof. Could anyone explain it to me, or provide some other proof that is close to this one in spirit? It is mentioned to be "a kind of diagnolization argument".

The proof can be found be on googlebooks(here, page 138-139). Here's a screenshot of it:  I like to think of this result in two parts, of which the first is the more subtle. The first part begins by recognizing that, in your hypothesis, the sets $X^k$ are internal but the sequence of them, i.e., the function $k\mapsto X^k$, is not known to be internal. (In fact, it's known not to be internal, because its domain is the set of standard natural numbers, which is not an internal set.) Nevertheless, this function can be extended to an internal function. That is, there is an internal function $G$, whose domain is the set ${}^*\mathbb N$ of all internal natural numbers (whether standard or not), such that $G(k)=X^k$ for all standard $k$. (At the moment, I'm not claiming anything about the values of $G(k)$ when $k$ is non-standard; that will come later.)
To produce $G$, proceed as follows. For each $k$, the internal entity $X^k$ is the equivalence class, modulo the ultrafilter $\mathcal F$, of some sequence $(z^k_n)_{n\in\mathbb N}$; fix such a sequence for each $k$. Now define, for each $n\in\mathbb N$, a function $g_n$ on $\mathbb N$ by setting $g_n(k)=z^k_n$. The sequence $(g_n)_{n\in\mathbb N}$ represents, modulo $\mathcal F$, an internal element $G$ of the ultrapower. I claim that this $G$ does what I claimed in the preceding paragraph. To see this, consider any standard natural number $k$; as an element of the ultrapower, it is represented by the constant function $n\mapsto k$. Using this, plus the fact that $G$ is represented by $n\mapsto g_n$, plus Los's theorem, we get that $G(k)$ is represented by the function $n\mapsto g_n(k)=z^k_n$. But that function was chosen to represent $X^k$. Therefore $G(k)=X^k$, for all standard $k$, as required.
That completes the first and hardest part of the proof. Notice, by the way, that it didn't matter that the $X^k$ were sets; they could have been any internal entities. Any $\mathbb N$-indexed sequence of internal entities can be extended to an internal ${}^*\mathbb N$-indexed sequence.
The second part of the proof is just an application of overspill. The statement "$G(k)$ is a nonempty set and is a subset of $G(j)$ for all $j<k$" is true for all standard $k$, because of the hypothesis that the $X^k$'s (for standard $k$) form a decreasing sequence of nonempty sets. By overspill, the same statement holds for some nonstandard $k$. But then any element of that $G(k)$ is in the intersection of all the earlier $G(j)$'s, which includes all the $X^j$'s for all standard $j$.