[proofplan] We prove the result directly by induction on formulas, rather than invoking the [Tarski-Vaught test](/theorems/4280) as a black box. The key point is that every finite tuple of parameters from the union already lies in some stage $M_k$, because the index set is directed. Atomic formulas are preserved because the interpretations in $M$ are induced from the compatible interpretations in the chain. The existential step uses directedness to put both the original parameters and a witness from $M$ into a common later structure, then uses elementarity inside the chain to pull the witness back to the chosen stage. [/proofplan] [step:Show that every finite tuple from the union lies in one stage] Fix $i_0 \in I$. We will prove that $M_{i_0} \preceq M$. First record the finite-tuple consequence of directedness. Let $a = (a_1,\dots,a_n) \in |M|^n$ be a finite tuple. For each $r \in \{1,\dots,n\}$, choose $i_r \in I$ such that $a_r \in |M_{i_r}|$. Since $(I,\leq)$ is directed, there exists $k \in I$ with \begin{align*} i_1 \leq k,\quad i_2 \leq k,\quad \dots,\quad i_n \leq k. \end{align*} Because $M_{i_r} \subseteq M_k$ for each $r$, we have $a \in |M_k|^n$. More generally, if $i \in I$ is fixed and $a \in |M_i|^m$, $b \in |M_j|^n$, then directedness gives $k \in I$ with $i \leq k$ and $j \leq k$, hence both tuples $a$ and $b$ lie in the common structure $M_k$. [/step] [step:Prove satisfaction equivalence by induction on formulas] We prove the following statement by induction on the complexity of an $L$-formula $\varphi(y_1,\dots,y_m)$: For every $i \in I$ and every tuple $a = (a_1,\dots,a_m) \in |M_i|^m$, \begin{align*} M_i \models \varphi(a) \quad \Longleftrightarrow \quad M \models \varphi(a). \end{align*} For atomic formulas, term evaluation is compatible with passage up the chain and with passage to $M$, because all function and constant symbols of $M$ are interpreted by the common compatible interpretations inherited from the $M_i$. Thus each atomic relation has the same truth value in $M_i$ and in $M$ on tuples from $M_i$. The Boolean connectives follow immediately from the induction hypothesis applied to the component formulas. It remains to handle existential quantification. Let $\varphi(y)$ be the formula \begin{align*} \exists x\, \psi(x,y), \end{align*} where $y = (y_1,\dots,y_m)$ is a finite tuple of free variables. Fix $i \in I$ and $a \in |M_i|^m$. Suppose first that \begin{align*} M_i \models \exists x\,\psi(x,a). \end{align*} Choose $c \in |M_i|$ such that $M_i \models \psi(c,a)$. By the induction hypothesis applied to $\psi$ with parameters $(c,a) \in |M_i|^{m+1}$, we get \begin{align*} M \models \psi(c,a), \end{align*} and therefore \begin{align*} M \models \exists x\,\psi(x,a). \end{align*} Conversely, suppose that \begin{align*} M \models \exists x\,\psi(x,a). \end{align*} Choose $b \in |M|$ such that $M \models \psi(b,a)$. By definition of $|M|$, there exists $j \in I$ with $b \in |M_j|$. Since $(I,\leq)$ is directed, choose $k \in I$ such that $i \leq k$ and $j \leq k$. Then $a \in |M_k|^m$ and $b \in |M_k|$. Applying the induction hypothesis to $\psi$ at the stage $k$ with parameters $(b,a) \in |M_k|^{m+1}$ gives \begin{align*} M_k \models \psi(b,a). \end{align*} Hence \begin{align*} M_k \models \exists x\,\psi(x,a). \end{align*} Because $i \leq k$, the hypothesis of the theorem gives $M_i \preceq M_k$. Therefore elementarity of the inclusion $M_i \hookrightarrow M_k$ yields \begin{align*} M_i \models \exists x\,\psi(x,a). \end{align*} This proves the existential step and completes the induction. [guided] We want to prove elementarity of $M_i \subseteq M$ for every fixed $i$, so we prove the full satisfaction equivalence for all formulas. The statement we induct on is: For every formula $\varphi(y_1,\dots,y_m)$, every index $i \in I$, and every tuple $a \in |M_i|^m$, \begin{align*} M_i \models \varphi(a) \quad \Longleftrightarrow \quad M \models \varphi(a). \end{align*} For atomic formulas, no model-theoretic argument is hidden. If a term is evaluated on a tuple from $M_i$, then every function symbol appearing in the term is interpreted in $M$ by the same compatible interpretation used in $M_i$. Thus the value of the term in $M_i$ is the same as its value in $M$. Relation symbols are also interpreted compatibly, so an atomic formula has the same truth value in $M_i$ and in $M$ on tuples from $M_i$. Negations, conjunctions, disjunctions, and implications are handled by applying the induction hypothesis to the smaller formulas and then using the truth tables for the connectives. The only substantive case is existential quantification. Let \begin{align*} \varphi(y) \equiv \exists x\,\psi(x,y), \end{align*} where $y = (y_1,\dots,y_m)$, and fix $i \in I$ and $a \in |M_i|^m$. First suppose \begin{align*} M_i \models \exists x\,\psi(x,a). \end{align*} Then there is a witness $c \in |M_i|$ such that \begin{align*} M_i \models \psi(c,a). \end{align*} The tuple $(c,a)$ lies in $|M_i|^{m+1}$, so the induction hypothesis applied to the smaller formula $\psi$ gives \begin{align*} M \models \psi(c,a). \end{align*} Therefore the same element $c$ witnesses \begin{align*} M \models \exists x\,\psi(x,a). \end{align*} Now suppose \begin{align*} M \models \exists x\,\psi(x,a). \end{align*} Choose a witness $b \in |M|$ with \begin{align*} M \models \psi(b,a). \end{align*} The element $b$ belongs to some stage $M_j$, because $|M|$ is the union of the underlying sets $|M_j|$. The parameters $a$ already lie in $M_i$. Directedness is used exactly here: choose $k \in I$ such that $i \leq k$ and $j \leq k$. Then both the parameters $a$ and the witness $b$ lie in $M_k$. Since $(b,a) \in |M_k|^{m+1}$, the induction hypothesis applied to $\psi$ at the stage $k$ gives \begin{align*} M_k \models \psi(b,a). \end{align*} Thus \begin{align*} M_k \models \exists x\,\psi(x,a). \end{align*} Because $i \leq k$, the chain hypothesis says that the inclusion $M_i \hookrightarrow M_k$ is elementary. Applying this elementarity to the formula $\exists x\,\psi(x,y)$ with parameter tuple $a \in |M_i|^m$, we obtain \begin{align*} M_i \models \exists x\,\psi(x,a). \end{align*} This proves the existential case, and hence the induction proves satisfaction equivalence for every first-order formula. [/guided] [/step] [step:Conclude that each stage is elementary in the union] Apply the satisfaction equivalence proved above with $i = i_0$. For every $L$-formula $\varphi(y_1,\dots,y_m)$ and every tuple $a \in |M_{i_0}|^m$, \begin{align*} M_{i_0} \models \varphi(a) \quad \Longleftrightarrow \quad M \models \varphi(a). \end{align*} This is precisely the definition that the inclusion map $M_{i_0} \hookrightarrow M$ is elementary. Since $i_0 \in I$ was arbitrary, $M_i \preceq M$ for every $i \in I$. [/step]