[proofplan] We prove the assertion by structural induction on the formula $\varphi$. The atomic cases are exactly the definitions of equality and membership in the ultrapower. The Boolean steps use the ultrafilter laws: closure under finite intersections and the fact that exactly one of a set and its complement belongs to an ultrafilter. The existential step is the only non-formal part: from a $U$-large set of indices admitting witnesses, the [axiom of choice](/page/Axiom%20of%20Choice) gives a witness function whose equivalence class realizes the existential formula in the ultrapower. [/proofplan] [step:Set up the induction statement for all assignments at once] For a formula $\psi(y_1,\dots,y_m)$, define the assertion $P(\psi)$ to mean the following statement: for every family of functions $g_1,\dots,g_m:I\to V$, \begin{align*} \operatorname{Ult}(V,U)\models \psi([g_1]_U,\dots,[g_m]_U) \iff \{i\in I : V\models \psi(g_1(i),\dots,g_m(i))\}\in U. \end{align*} We prove $P(\psi)$ for every first-order formula $\psi$ by induction on formula complexity, using atomic formulas, negation, conjunction, and existential quantification as the primitive formation rules. Other Boolean connectives and universal quantifiers are abbreviations in terms of these primitives. All satisfaction assertions below are read in the ambient metatheory for the fixed formula under discussion, using the usual recursive definition of satisfaction for that formula. Thus the proof does not require an internal truth predicate for the universe $V$. We also use the standard cumulative hierarchy notation: $V_\eta$ denotes the $\eta$-th rank level, and the rank of a set $a$ is the least ordinal $\eta$ such that $a\subseteq V_\eta$. [/step] [step:Check that the quotient relations are well defined] First, $=_U$ is an [equivalence relation](/page/Equivalence%20Relation) because $U$ contains $I$, is closed under finite intersections, and is upward closed. Reflexivity is immediate; symmetry is immediate; and transitivity follows because if $f=_U g$ and $g=_U h$, then $\{i:f(i)=g(i)\}\cap\{i:g(i)=h(i)\}\subseteq\{i:f(i)=h(i)\}$. The interpreted membership relation is independent of representatives. Suppose $f=_U f'$ and $g=_U g'$. Let \begin{align*} E:=\{i\in I:f(i)=f'(i)\}\cap\{i\in I:g(i)=g'(i)\}. \end{align*} Then $E\in U$. On every $i\in E$, one has $f(i)\in g(i)$ if and only if $f'(i)\in g'(i)$. Therefore the two membership truth sets agree on a $U$-large set: \begin{align*} E\cap\{i:f(i)\in g(i)\}=E\cap\{i:f'(i)\in g'(i)\}. \end{align*} Equivalently, their symmetric difference is contained in $I\setminus E$, which is not in $U$. Hence \begin{align*} \{i:f(i)\in g(i)\}\in U \iff \{i:f'(i)\in g'(i)\}\in U. \end{align*} Thus $\in_U$ is a well-defined relation on $=_U$-equivalence classes, so the ultrapower structure used in the induction is meaningful. [/step] [step:Verify atomic equality and membership from the ultrapower definitions] Let $g,h:I\to V$ be functions. For the atomic formula $y_1=y_2$, satisfaction in the ultrapower means equality of equivalence classes: \begin{align*} \operatorname{Ult}(V,U)\models [g]_U=[h]_U \iff [g]_U=[h]_U. \end{align*} By the definition of $=_U$ and of the quotient class, \begin{align*} [g]_U=[h]_U \iff \{i\in I:g(i)=h(i)\}\in U. \end{align*} Thus $P(y_1=y_2)$ holds. For the atomic formula $y_1\in y_2$, satisfaction in $\operatorname{Ult}(V,U)$ uses the interpreted membership relation $\in_U$: \begin{align*} \operatorname{Ult}(V,U)\models [g]_U\in [h]_U \iff [g]_U\in_U [h]_U. \end{align*} By the definition of $\in_U$, \begin{align*} [g]_U\in_U [h]_U \iff \{i\in I:g(i)\in h(i)\}\in U. \end{align*} Hence $P(y_1\in y_2)$ holds. The same arguments handle arbitrary atomic formulas $y_j=y_k$ and $y_j\in y_k$ by applying the equality or membership case to the corresponding functions in the assignment. [/step] [step:Pass the induction through negation using ultrafilter complements] Assume $P(\psi)$ holds for a formula $\psi(y_1,\dots,y_m)$, and let $g_1,\dots,g_m:I\to V$ be functions. Define the subset $A_\psi\subset I$ by \begin{align*} A_\psi:=\{i\in I:V\models \psi(g_1(i),\dots,g_m(i))\}. \end{align*} Then \begin{align*} \{i\in I:V\models \neg\psi(g_1(i),\dots,g_m(i))\}=I\setminus A_\psi. \end{align*} By the semantics of negation in $\operatorname{Ult}(V,U)$, \begin{align*} \operatorname{Ult}(V,U)\models \neg\psi([g_1]_U,\dots,[g_m]_U) \iff \operatorname{Ult}(V,U)\not\models \psi([g_1]_U,\dots,[g_m]_U). \end{align*} Using the induction hypothesis, the right-hand side is equivalent to $A_\psi\notin U$. Since $U$ is an ultrafilter on $I$, exactly one of $A_\psi$ and $I\setminus A_\psi$ belongs to $U$. Therefore \begin{align*} A_\psi\notin U \iff I\setminus A_\psi\in U. \end{align*} This proves $P(\neg\psi)$. [guided] We want to compare truth of $\neg\psi$ in the ultrapower with truth of $\neg\psi$ on a $U$-large set of indices. The right set to isolate is the truth set for $\psi$ itself. Define \begin{align*} A_\psi:=\{i\in I:V\models \psi(g_1(i),\dots,g_m(i))\}. \end{align*} Then the truth set for $\neg\psi$ is its complement: \begin{align*} \{i\in I:V\models \neg\psi(g_1(i),\dots,g_m(i))\}=I\setminus A_\psi. \end{align*} Now use the semantics of negation in the ultrapower: \begin{align*} \operatorname{Ult}(V,U)\models \neg\psi([g_1]_U,\dots,[g_m]_U) \iff \operatorname{Ult}(V,U)\not\models \psi([g_1]_U,\dots,[g_m]_U). \end{align*} The induction hypothesis applies to $\psi$ with the assignment represented by $g_1,\dots,g_m$, so \begin{align*} \operatorname{Ult}(V,U)\models \psi([g_1]_U,\dots,[g_m]_U) \iff A_\psi\in U. \end{align*} Negating both sides gives that the ultrapower satisfies $\neg\psi$ exactly when $A_\psi\notin U$. The ultrafilter property is precisely what converts non-membership of $A_\psi$ into membership of its complement. Since $U$ is an ultrafilter, exactly one of $A_\psi$ and $I\setminus A_\psi$ lies in $U$. Hence \begin{align*} A_\psi\notin U \iff I\setminus A_\psi\in U. \end{align*} But $I\setminus A_\psi$ is the set of indices where $V$ satisfies $\neg\psi$. Therefore $P(\neg\psi)$ holds. [/guided] [/step] [step:Pass the induction through conjunction using finite intersections] Assume $P(\psi)$ and $P(\theta)$ hold for formulas $\psi(y_1,\dots,y_m)$ and $\theta(y_1,\dots,y_m)$, and let $g_1,\dots,g_m:I\to V$ be functions. Define subsets $A_\psi,A_\theta\subset I$ by \begin{align*} A_\psi:=\{i\in I:V\models \psi(g_1(i),\dots,g_m(i))\} \end{align*} and \begin{align*} A_\theta:=\{i\in I:V\models \theta(g_1(i),\dots,g_m(i))\}. \end{align*} The truth set for the conjunction is \begin{align*} \{i\in I:V\models (\psi\wedge\theta)(g_1(i),\dots,g_m(i))\}=A_\psi\cap A_\theta. \end{align*} By the semantics of conjunction in $\operatorname{Ult}(V,U)$ and the induction hypotheses, \begin{align*} \operatorname{Ult}(V,U)\models (\psi\wedge\theta)([g_1]_U,\dots,[g_m]_U) \iff A_\psi\in U \text{ and } A_\theta\in U. \end{align*} Since $U$ is a filter, $A_\psi\in U$ and $A_\theta\in U$ imply $A_\psi\cap A_\theta\in U$. Conversely, since $A_\psi\cap A_\theta\subset A_\psi$ and $A_\psi\cap A_\theta\subset A_\theta$, upward closure of $U$ implies that $A_\psi\cap A_\theta\in U$ gives $A_\psi\in U$ and $A_\theta\in U$. Therefore \begin{align*} \operatorname{Ult}(V,U)\models (\psi\wedge\theta)([g_1]_U,\dots,[g_m]_U) \iff A_\psi\cap A_\theta\in U. \end{align*} This proves $P(\psi\wedge\theta)$. [/step] [step:Pass the induction through existential quantification using a witness function] Assume $P(\psi)$ holds for a formula $\psi(y,z_1,\dots,z_m)$, and let $g_1,\dots,g_m:I\to V$ be functions. Define $B\subset I$ by \begin{align*} B:=\{i\in I:V\models \exists y\,\psi(y,g_1(i),\dots,g_m(i))\}. \end{align*} We prove that \begin{align*} \operatorname{Ult}(V,U)\models \exists y\,\psi(y,[g_1]_U,\dots,[g_m]_U) \iff B\in U. \end{align*} First suppose $\operatorname{Ult}(V,U)\models \exists y\,\psi(y,[g_1]_U,\dots,[g_m]_U)$. Then there is a function $h:I\to V$ such that \begin{align*} \operatorname{Ult}(V,U)\models \psi([h]_U,[g_1]_U,\dots,[g_m]_U). \end{align*} By the induction hypothesis applied to $\psi$, \begin{align*} A_h:=\{i\in I:V\models \psi(h(i),g_1(i),\dots,g_m(i))\}\in U. \end{align*} For every $i\in A_h$, the element $h(i)$ witnesses the existential formula in $V$, so $A_h\subset B$. Since $U$ is upward closed and $A_h\in U$, it follows that $B\in U$. Conversely suppose $B\in U$. For each $i\in B$, choose witnesses in a set-sized way as follows. Among all sets $a$ satisfying $V\models \psi(a,g_1(i),\dots,g_m(i))$, let $\rho_i$ denote the least possible rank of such a witness. The witnesses of rank $\rho_i$ form a nonempty subset of the set $V_{\rho_i+1}$. Since $\psi$ is fixed, the satisfaction relation for $\psi$ is a definable predicate in the ambient metatheory; hence Replacement and Separation form these nonempty witness sets as a set-indexed family over $B$. The axiom of choice gives an element $a_i$ from the $i$th witness set. Thus, for every $i\in B$, \begin{align*} V\models \psi(a_i,g_1(i),\dots,g_m(i)). \end{align*} Choose an arbitrary set $a_0\in V$, for instance $a_0=\varnothing$, and define a function $h:I\to V$ by setting $h(i)=a_i$ for $i\in B$ and $h(i)=a_0$ for $i\in I\setminus B$. Then \begin{align*} B\subset \{i\in I:V\models \psi(h(i),g_1(i),\dots,g_m(i))\}. \end{align*} Because $B\in U$ and $U$ is upward closed, the larger truth set belongs to $U$. By the induction hypothesis applied to $\psi$, \begin{align*} \operatorname{Ult}(V,U)\models \psi([h]_U,[g_1]_U,\dots,[g_m]_U). \end{align*} Therefore \begin{align*} \operatorname{Ult}(V,U)\models \exists y\,\psi(y,[g_1]_U,\dots,[g_m]_U). \end{align*} This proves $P(\exists y\,\psi)$. [guided] The existential case has two directions, and they express the same idea from opposite sides: witnesses in the ultrapower are represented by functions, while $U$-many pointwise witnesses can be assembled into one representing function. Define the pointwise existential truth set \begin{align*} B:=\{i\in I:V\models \exists y\,\psi(y,g_1(i),\dots,g_m(i))\}. \end{align*} We first assume the ultrapower satisfies the existential formula: \begin{align*} \operatorname{Ult}(V,U)\models \exists y\,\psi(y,[g_1]_U,\dots,[g_m]_U). \end{align*} By the semantics of the existential quantifier in the ultrapower structure, there is an element of the ultrapower domain witnessing the formula. Every element of that domain has the form $[h]_U$ for some function $h:I\to V$. Thus there exists $h:I\to V$ such that \begin{align*} \operatorname{Ult}(V,U)\models \psi([h]_U,[g_1]_U,\dots,[g_m]_U). \end{align*} Now apply the induction hypothesis to the smaller formula $\psi$ and the functions $h,g_1,\dots,g_m$. It gives \begin{align*} A_h:=\{i\in I:V\models \psi(h(i),g_1(i),\dots,g_m(i))\}\in U. \end{align*} Whenever $i\in A_h$, the specific set $h(i)$ is a witness to $\exists y\,\psi(y,g_1(i),\dots,g_m(i))$ in $V$. Hence $A_h\subset B$. Since $U$ is upward closed, $A_h\in U$ and $A_h\subset B$ imply $B\in U$. For the converse, assume $B\in U$. This means that for $U$-many indices $i$, there exists at least one set witnessing $\psi(y,g_1(i),\dots,g_m(i))$ in $V$. To keep the choice set-sized, do not choose from the whole class of witnesses. Instead, for each $i\in B$, let $\rho_i$ denote the least possible rank of a witness, and define the minimal-rank witness set \begin{align*} W_i:=\{a\in V_{\rho_i+1}:V\models \psi(a,g_1(i),\dots,g_m(i)) \text{ and } a \text{ has rank } \rho_i\}. \end{align*} Each $W_i$ is a nonempty set, and Replacement gives the set-indexed family $(W_i)_{i\in B}$. Using the axiom of choice for this family, choose $a_i\in W_i$ for each $i\in B$. Choose a fixed default set $a_0:=\varnothing$ for indices outside $B$, and define the function $h:I\to V$ by the rule: $h(i)=a_i$ if $i\in B$, and $h(i)=a_0$ if $i\in I\setminus B$. For every $i\in B$, the choice $a_i\in W_i$ gives \begin{align*} V\models \psi(h(i),g_1(i),\dots,g_m(i)). \end{align*} Therefore \begin{align*} B\subset \{i\in I:V\models \psi(h(i),g_1(i),\dots,g_m(i))\}. \end{align*} Since $B\in U$ and $U$ is upward closed, the truth set on the right belongs to $U$. Applying the induction hypothesis to $\psi$ once more yields \begin{align*} \operatorname{Ult}(V,U)\models \psi([h]_U,[g_1]_U,\dots,[g_m]_U). \end{align*} Thus the equivalence class $[h]_U$ is a witness in the ultrapower, so \begin{align*} \operatorname{Ult}(V,U)\models \exists y\,\psi(y,[g_1]_U,\dots,[g_m]_U). \end{align*} This proves the existential step. [/guided] [/step] [step:Conclude the theorem for the given formula] The structural induction proves $P(\psi)$ for every first-order formula $\psi$ in the language of set theory. Applying this result to the given formula $\varphi(x_1,\dots,x_n)$ and to the functions $f_1,\dots,f_n:I\to V$ gives \begin{align*} \operatorname{Ult}(V,U)\models \varphi([f_1]_U,\dots,[f_n]_U) \iff \{i\in I:V\models \varphi(f_1(i),\dots,f_n(i))\}\in U. \end{align*} This is the desired equivalence. [/step]