Model-theoretic ultralimit

An ultralimit is the direct limit of a chain of structures formed by taking successive ultrapowers along their diagonal elementary embeddings. At limit stages use the elementary chain theorem. This is a different concept from a topological ultrafilter limit. Alternating relative ultrapower embeddings constructs isomorphic ultralimits of any two elementarily equivalent structures, without requiring the stronger single-ultrapower isomorphism theorem.

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⪯A_1⪯B_1⪯A_2⪯B_2⪯\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.

If $A\equiv B$, the elementary diagram of $B$ is finitely satisfiable by interpreting its finitely many named elements in $A$. Choose those finite realizations as coordinates, extend the filter of diagram cones to an ultrafilter, and use the Łoś theorem to embed $B$ elementarily into an ultrapower of $A$. If $A\prec B$, work over the named elements of $A$ and keep their coordinates constant. The resulting embedding extends the diagonal map of $A$. This relative assertion allows an alternating chain of ultrapowers to keep every previously embedded substructure fixed.