[proofplan]
We first verify that $\sim_{\mathcal U}$ is an [equivalence relation](/page/Equivalence%20Relation), so the quotient set used as the universe is well defined. We then show that replacing representatives by $\mathcal U$-equivalent representatives does not change any interpreted symbol. Constants require no representative choice; function symbols respect coordinate agreement on a $\mathcal U$-large finite intersection; and relation symbols have truth sets whose membership in $\mathcal U$ is unchanged after modification on a non-$\mathcal U$-large set. The argument uses only the filter properties of $\mathcal U$, so the well-definedness conclusion in fact holds for any filter, while the theorem states the standard ultraproduct case of an ultrafilter.
[/proofplan]
[step:Verify that $\sim_{\mathcal U}$ is an equivalence relation]
Define a binary relation $\sim_{\mathcal U}$ on $\prod_{i \in I} M_i$ by declaring, for $a,b \in \prod_{i \in I} M_i$,
\begin{align*}
a \sim_{\mathcal U} b
\quad \Longleftrightarrow \quad
\{i \in I : a_i = b_i\} \in \mathcal U.
\end{align*}
Since $\mathcal U$ is an ultrafilter on $I$, it is a filter on $I$; hence $I \in \mathcal U$, $\mathcal U$ is closed under finite intersections, and $\mathcal U$ is upward closed under inclusion.
For reflexivity, let $a \in \prod_{i \in I} M_i$. Then $\{i \in I : a_i = a_i\} = I \in \mathcal U$, so $a \sim_{\mathcal U} a$. For symmetry, if $a \sim_{\mathcal U} b$, then
\begin{align*}
\{i \in I : b_i = a_i\} = \{i \in I : a_i = b_i\} \in \mathcal U,
\end{align*}
so $b \sim_{\mathcal U} a$. For transitivity, suppose $a \sim_{\mathcal U} b$ and $b \sim_{\mathcal U} c$. Define
\begin{align*}
A &:= \{i \in I : a_i = b_i\},\\
B &:= \{i \in I : b_i = c_i\}.
\end{align*}
Then $A,B \in \mathcal U$, so $A \cap B \in \mathcal U$. If $i \in A \cap B$, then $a_i=b_i=c_i$, and therefore
\begin{align*}
A \cap B \subset \{i \in I : a_i = c_i\}.
\end{align*}
By upward closure, $\{i \in I : a_i = c_i\} \in \mathcal U$, so $a \sim_{\mathcal U} c$. Thus $\sim_{\mathcal U}$ is an equivalence relation, and the quotient $\prod_{i \in I} M_i/\mathcal U$ is well defined as a set of equivalence classes.
[/step]
[step:Verify that constant symbols are independent of representatives]
Let $c \in L$ be a constant symbol. The interpretation
\begin{align*}
c^M := [(c^{M_i})_{i \in I}]_{\mathcal U}
\end{align*}
uses the distinguished element $c^{M_i} \in M_i$ in each coordinate and does not involve any input representative. Hence the interpretation of $c$ is a single well-defined element of $M$.
[/step]
[step:Show that coordinatewise function symbols respect $\mathcal U$-equivalence]
Let $f \in L$ be an $n$-ary function symbol. Let
\begin{align*}
a_k, \tilde a_k \in \prod_{i \in I} M_i
\end{align*}
for $1 \leq k \leq n$, and suppose
\begin{align*}
[a_k]_{\mathcal U} = [\tilde a_k]_{\mathcal U}
\end{align*}
for every $1 \leq k \leq n$. For each $k$, define the coordinate agreement set
\begin{align*}
A_k := \{i \in I : (a_k)_i = (\tilde a_k)_i\}.
\end{align*}
By the definition of $\sim_{\mathcal U}$, each $A_k$ belongs to $\mathcal U$. Since $\mathcal U$ is a filter and filters are closed under finite intersections, the set
\begin{align*}
A := \bigcap_{k=1}^n A_k
\end{align*}
belongs to $\mathcal U$.
Define two elements $b,\tilde b \in \prod_{i \in I} M_i$ by
\begin{align*}
b_i &:= f^{M_i}((a_1)_i,\dots,(a_n)_i),\\
\tilde b_i &:= f^{M_i}((\tilde a_1)_i,\dots,(\tilde a_n)_i)
\end{align*}
for each $i \in I$. If $i \in A$, then $(a_k)_i = (\tilde a_k)_i$ for every $k$, so
\begin{align*}
b_i = \tilde b_i.
\end{align*}
Thus
\begin{align*}
A \subset \{i \in I : b_i = \tilde b_i\}.
\end{align*}
Because $\mathcal U$ is closed upward and $A \in \mathcal U$, we have
\begin{align*}
\{i \in I : b_i = \tilde b_i\} \in \mathcal U.
\end{align*}
Therefore $b \sim_{\mathcal U} \tilde b$, so
\begin{align*}
[(f^{M_i}((a_1)_i,\dots,(a_n)_i))_{i \in I}]_{\mathcal U}
=
[(f^{M_i}((\tilde a_1)_i,\dots,(\tilde a_n)_i))_{i \in I}]_{\mathcal U}.
\end{align*}
Hence $f^M$ is independent of the chosen representatives.
[/step]
[step:Prove that relation truth sets are unchanged by $\mathcal U$-large agreement]
Let $R \in L$ be an $n$-ary relation symbol. Let
\begin{align*}
a_k, \tilde a_k \in \prod_{i \in I} M_i
\end{align*}
for $1 \leq k \leq n$, and suppose $[a_k]_{\mathcal U} = [\tilde a_k]_{\mathcal U}$ for every $k$. Define
\begin{align*}
A_k &:= \{i \in I : (a_k)_i = (\tilde a_k)_i\},\\
A &:= \bigcap_{k=1}^n A_k.
\end{align*}
As before, $A \in \mathcal U$.
For each $i \in I$, let $R^{M_i} \subset M_i^n$ denote the interpretation of the relation symbol $R$ in the $L$-structure $M_i$. Define the two relation truth sets
\begin{align*}
S &:= \{i \in I : M_i \models R((a_1)_i,\dots,(a_n)_i)\},\\
T &:= \{i \in I : M_i \models R((\tilde a_1)_i,\dots,(\tilde a_n)_i)\}.
\end{align*}
Equivalently, $i \in S$ exactly when $((a_1)_i,\dots,(a_n)_i) \in R^{M_i}$, and $i \in T$ exactly when $((\tilde a_1)_i,\dots,(\tilde a_n)_i) \in R^{M_i}$. For every $i \in A$, the two coordinate tuples are equal:
\begin{align*}
((a_1)_i,\dots,(a_n)_i)
=
((\tilde a_1)_i,\dots,(\tilde a_n)_i).
\end{align*}
Since $R^{M_i}$ is a relation on $M_i$, equal tuples have the same truth value. Hence
\begin{align*}
S \cap A = T \cap A.
\end{align*}
We now prove $S \in \mathcal U \iff T \in \mathcal U$. If $S \in \mathcal U$, then $S \cap A \in \mathcal U$ by closure under finite intersections. Since $S \cap A = T \cap A$ and $T \cap A \subset T$, closure upward gives $T \in \mathcal U$. Conversely, if $T \in \mathcal U$, then $T \cap A \in \mathcal U$ by closure under finite intersections. Since $T \cap A = S \cap A$ and $S \cap A \subset S$, closure upward gives $S \in \mathcal U$. Therefore
\begin{align*}
S \in \mathcal U \iff T \in \mathcal U.
\end{align*}
Thus the truth value of
\begin{align*}
R([a_1]_{\mathcal U},\dots,[a_n]_{\mathcal U})
\end{align*}
is independent of the chosen representatives.
[/step]
[step:Assemble the interpretations into an $L$-structure]
The quotient set $M=\prod_{i \in I}M_i/\mathcal U$ is the underlying set; this quotient is legitimate because $\sim_{\mathcal U}$ was verified to be an equivalence relation. The previous steps show that each constant symbol, function symbol, and relation symbol of $L$ has an interpretation on $M$ that is independent of every representative choice. In those verifications we used only that $\mathcal U$ is a filter, namely that it contains $I$, is closed under finite intersections, and is upward closed under inclusion; these properties follow from the hypothesis that $\mathcal U$ is an ultrafilter. Therefore the coordinatewise interpretations define a well-defined $L$-structure on $\prod_{i \in I} M_i/\mathcal U$, as required.
[/step]
