Alternating ultrapowers give isomorphic ultralimits (source code)

= Alternating ultrapowers give isomorphic ultralimits
{title2=$A\equiv B\Longrightarrow A_\infty\cong B_\infty$}

= Frayne theorem
{c}
{synonym}

The <Frayne embedding lemma> embeds $B$ into an <ultrapower> $A_1$ of $A$. Its relative version embeds $A_1$ into an ultrapower $B_1$ of $B$, fixing the diagonal copy of $B$. Continue alternately over the previously fixed elementary substructure. After coherent identifications one has $B\preceq A_1\preceq B_1\preceq A_2\preceq B_2\preceq\cdots$, while each $A_{n+1}$ is an ultrapower of $A_n$ along its diagonal map, and similarly for $B$. The two cofinal subsequences have the same elementary union. This proves the ultralimit assertion without the stronger single-ultrapower isomorphism theorem.