Keisler Order: Saturated Ultrapowers Keisler's paper "Ultraproducts which are not Saturated" states the following theorem as a corollary to a (much more) generalized theorem. However, I cannot figure out how to prove it for the specific case. 
Theorem: Let $D$ be a regular ultrafilter over $I$ (where $|I| =\alpha$) and let $\mathfrak{A} \equiv \mathfrak{B}$. Then the ultrapowers $\prod_D\mathfrak{A}$ is $\alpha^+$-saturated iff $\prod_D \mathfrak{B}$ is $\alpha^+$-saturated. 
Information:
Recall that since $D$ is regular there exists a countable subset $X$ of $D$ such that $\bigcap X=\emptyset$. Let $a$ be an $\alpha$-sized collection of $\alpha$-termed sequence in  $\prod_D \mathfrak{A}$ and let $\Sigma(x)$ be a collection of formulas in one-free variable (of power $\alpha$) which is finitely satisfiable in $(\prod_D \mathfrak{A},a)$. It suffices to show that if $\prod_D\mathfrak{A}$ realizes $\Sigma(x)$ then $\prod_D \mathfrak{B}$ realizes $\Sigma(x)$. 
Thank you.
 A: I'm assuming you didn't want to appeal to the general theorem, since the corollary is essentially just a restatement with $\beta = \alpha = \omega$. I think a direct approach would simply amount to understanding that the realization of a type in an ultrapower is essentially a combinatorial property of the way the realizations of sentences cohere in the ultrafilter. Here's the proof I've seen of this (I suspect it's nothing more than Keisler's argument wearing a different hat, but hopefully it helps).
Since $D$ is $(\omega, \alpha)$-regular by hypothesis, there is a family of size $\alpha$ for which every countable subset has empty intersection. Let $\{X_i\}_{i \in I}$ be this family.
Define the Łoś map for the type $\Sigma(x) = \{ \phi_i(x) \mid i \in I \}$:
\begin{align*}
f: [\alpha]^{< \aleph_0} &\rightarrow D \\
\sigma &\mapsto \{t \in I \mid \mathfrak{A}_t \vDash \exists x \bigwedge_{n \in \sigma} \phi_n(x) \} \cap \bigcap_{n \in \sigma} X_n
\end{align*}
mapping finite subsets of $\alpha$ (which correspond to finite conjunctions of sentences in $\Sigma(x)$) to the set of indices on which they are simultaneously realized ('normalized' by the regular family for control). Finite satisfiability of $\Sigma(x)$ in the ultrapower says the above map is well-defined.
Now say $\Sigma(x)$ is realized by $a = [a_i]_{i \in I}$ in the ultrapower. We can construct a map $g$ as above (from finite subsets of $\alpha$ into the ultrafilter) that 'refines' $f$ in the sense that $g(\sigma) \subset f(\sigma)$ for all finite subsets $\sigma \subset \alpha$ (and, of course, we require $g$ to still map into $D$). Do this by letting $g(\{s\}) = \{t \in I \mid \mathfrak{A}_t \vDash \phi_s(a_t)\} \cap X_s$ and extending by declaring $g(u \cup v) = g(u) \cap g(v)$ (call this last property 'multiplicativity'). The fact that $a$ realizes $\Sigma(x)$ says that extending $g$ by multiplicativity still maps into subsets of the ultrafilter and that $g$ refines $f$ (you should check these for yourself). So if $\Sigma(x)$ is realized in the ultrapower, $f$ has a multiplicative refinement.
Conversely, suppose $f$ had a multiplicative refinement, $g$. Because $D$ is regular with $\{X_n\}$, so is the image of $g$, hence the set $\{ \sigma \mid t \in g(\sigma) \}$ is finite for any given $t \in I$ (if it were infinite, we would have infinitely many $X_n$'s occurring in an intersection that would have to contain $t$). 
Now, to build a realization for $\Sigma(x)$, we just pick for each $t \in I$ a common realization $a_t$ for all the finitely many $\{ \phi_i(x) \mid i \in \sigma, t \in g(\sigma)\}$. Multiplicativity of $g$ says exactly that this is possible. Now just observe that $a = [a_t]_{t \in I}$ realizes $\Sigma(x)$ in the ultrapower.
Since I was asked to elaborate on how this helps: specifically, if $\Sigma(x)$ is realized in the ultrapower $\mathfrak{A}^\alpha/D$, then the map $f$ above has a multiplicative refinement. If you read the definition of $f$, it is easy to see that replacing $\mathfrak{A}_t$ with elementarily equivalent copies $\mathfrak{B}_t$ gives you the same map $f$. 
Even better, say you had a parameter set $B$ of cardinality at most  $\alpha$ in your ultrapower $\mathfrak{B}^\alpha/D$, and you knew that $\mathfrak{A}^\alpha/D$ was saturated for all types over sets of cardinality $\kappa \leq \alpha$. Fix representatives for $B$ and project them down to models $\mathfrak{B}_t$. While the model $\mathfrak{A}_t$ doesn't understand what $b_t$ (the projection of a representative $b$ in $B$) is, it knows nevertheless that $\exists y \phi(x, y)$ is a satisfiable formula, so pick whatever you want for $y$ that makes it work. Since $t$ is only in finitely many $X_n$, you only need to worry about finitely many formulas at a given $t$. Doing this, you will have constructed an analogous type with a corresponding $f'$ in $\mathfrak{A}^\alpha/D$ over a new set $A$ of cardinality at most $|B|$. A multiplicative refinement here will correspond to a multiplicative refinement of the original $f$.
