[proofplan] We prove a slightly stronger assignment version: for every variable assignment $s$ in $M$, satisfaction of any formula is preserved when the assignment is transported through the isomorphism $h$. The proof proceeds by induction on terms first, showing that term evaluation commutes with $h$. We then prove the formula statement by structural induction, using preservation of relation symbols for atomic formulas, elementary logic for Boolean connectives, and bijectivity of $h$ for quantifiers. The desired tuple statement follows by choosing an assignment sending each $x_i$ to $a_i$. [/proofplan]

[step:Transport variable assignments through the isomorphism] Let $\operatorname{Var}$ denote the set of first-order variables of the language. For an assignment \begin{align*} s: \operatorname{Var} \to |M|, \end{align*} define the transported assignment \begin{align*} h_\ast s: \operatorname{Var} \to |N| \end{align*} by \begin{align*} (h_\ast s)(x) := h(s(x)) \end{align*} for every variable $x \in \operatorname{Var}$. For a variable $y \in \operatorname{Var}$ and an element $b \in |M|$, write $s[y \mapsto b]$ for the assignment into $|M|$ that sends $y$ to $b$ and agrees with $s$ on all variables different from $y$. Similarly, for $c \in |N|$, write $(h_\ast s)[y \mapsto c]$ for the corresponding assignment into $|N|$. [/step]

[step:Show that term evaluation commutes with the isomorphism]We prove that for every $L$-term $\tau$ and every assignment $s: \operatorname{Var} \to |M|$, \begin{align*} \tau^N(h_\ast s) = h(\tau^M(s)), \end{align*} where $\tau^M(s) \in |M|$ and $\tau^N(h_\ast s) \in |N|$ denote the interpretations of $\tau$ in $M$ and $N$ under the indicated assignments. We argue by induction on the construction of $\tau$. If $\tau$ is a variable $x$, then \begin{align*} \tau^N(h_\ast s) = (h_\ast s)(x) = h(s(x)) = h(\tau^M(s)). \end{align*} If $\tau$ is a constant symbol $c$ of $L$, then, because $h$ is an $L$-isomorphism, it preserves constants: \begin{align*} h(c^M) = c^N. \end{align*} Therefore \begin{align*} \tau^N(h_\ast s) = c^N = h(c^M) = h(\tau^M(s)). \end{align*} Now suppose $\tau$ has the form $f(\tau_1,\dots,\tau_m)$, where $f$ is an $m$-ary function symbol of $L$ and $\tau_1,\dots,\tau_m$ are $L$-terms. By the induction hypothesis, for each $j \in \{1,\dots,m\}$, \begin{align*} \tau_j^N(h_\ast s) = h(\tau_j^M(s)). \end{align*} Since $h$ is an $L$-isomorphism, it preserves the interpretation of $f$: \begin{align*} h\bigl(f^M(b_1,\dots,b_m)\bigr) = f^N(h(b_1),\dots,h(b_m)) \end{align*} for all $b_1,\dots,b_m \in |M|$. Applying this with $b_j := \tau_j^M(s)$ gives \begin{align*} \tau^N(h_\ast s) &= f^N(\tau_1^N(h_\ast s),\dots,\tau_m^N(h_\ast s)) \\ &= f^N(h(\tau_1^M(s)),\dots,h(\tau_m^M(s))) \\ &= h\bigl(f^M(\tau_1^M(s),\dots,\tau_m^M(s))\bigr) \\ &= h(\tau^M(s)). \end{align*} This completes the induction on terms.[/step]

[guided]The purpose of this step is to prove that every term has the same value after transporting it through the isomorphism. Formally, for every $L$-term $\tau$ and every assignment $s: \operatorname{Var} \to |M|$, we want \begin{align*} \tau^N(h_\ast s) = h(\tau^M(s)). \end{align*} We prove this by induction on how the term is built. If the term is a variable $x$, its interpretation in $M$ is $s(x)$, while its interpretation in $N$ under the transported assignment is \begin{align*} (h_\ast s)(x) = h(s(x)). \end{align*} Thus the identity holds for variables. If the term is a constant symbol $c$, then the defining property of an $L$-isomorphism says that $h$ carries the interpretation of $c$ in $M$ to the interpretation of $c$ in $N$: \begin{align*} h(c^M) = c^N. \end{align*} Since the value of the constant term $c$ is $c^M$ in $M$ and $c^N$ in $N$, this gives \begin{align*} c^N = h(c^M). \end{align*} Finally, suppose the term is built from an $m$-ary function symbol $f$ as \begin{align*} \tau = f(\tau_1,\dots,\tau_m). \end{align*} The induction hypothesis tells us that each subterm commutes with $h$: \begin{align*} \tau_j^N(h_\ast s) = h(\tau_j^M(s)) \end{align*} for every $j \in \{1,\dots,m\}$. Since $h$ is an $L$-isomorphism, it also preserves the interpretation of $f$: \begin{align*} h\bigl(f^M(b_1,\dots,b_m)\bigr) = f^N(h(b_1),\dots,h(b_m)) \end{align*} for all $b_1,\dots,b_m \in |M|$. Substituting $b_j := \tau_j^M(s)$, we get \begin{align*} \tau^N(h_\ast s) &= f^N(\tau_1^N(h_\ast s),\dots,\tau_m^N(h_\ast s)) \\ &= f^N(h(\tau_1^M(s)),\dots,h(\tau_m^M(s))) \\ &= h\bigl(f^M(\tau_1^M(s),\dots,\tau_m^M(s))\bigr) \\ &= h(\tau^M(s)). \end{align*} Thus term evaluation commutes with the isomorphism for every term.[/guided]

[step:Prove invariance for atomic formulas] We prove the assignment-level satisfaction equivalence for atomic formulas. First let $\psi$ be the atomic formula $\tau_1 = \tau_2$, where $\tau_1$ and $\tau_2$ are $L$-terms. By the term invariance just proved, \begin{align*} \tau_1^N(h_\ast s) = h(\tau_1^M(s)), \qquad \tau_2^N(h_\ast s) = h(\tau_2^M(s)). \end{align*} Since $h$ is injective, \begin{align*} \tau_1^M(s) = \tau_2^M(s) \iff h(\tau_1^M(s)) = h(\tau_2^M(s)). \end{align*} Therefore \begin{align*} M \models \tau_1 = \tau_2 [s] \iff N \models \tau_1 = \tau_2 [h_\ast s]. \end{align*} Now let $\psi$ be the atomic formula $R(\tau_1,\dots,\tau_m)$, where $R$ is an $m$-ary relation symbol of $L$. By term invariance, \begin{align*} \tau_j^N(h_\ast s) = h(\tau_j^M(s)) \end{align*} for every $j \in \{1,\dots,m\}$. Since $h$ is an $L$-isomorphism, it preserves and reflects the interpretation of $R$: \begin{align*} (\tau_1^M(s),\dots,\tau_m^M(s)) \in R^M \iff (h(\tau_1^M(s)),\dots,h(\tau_m^M(s))) \in R^N. \end{align*} Hence \begin{align*} M \models R(\tau_1,\dots,\tau_m)[s] \iff N \models R(\tau_1,\dots,\tau_m)[h_\ast s]. \end{align*} [/step]

[step:Extend the equivalence through Boolean connectives] Assume the assignment-level equivalence has been proved for formulas $\alpha$ and $\beta$. For negation, \begin{align*} M \models \neg \alpha [s] &\iff \text{not } M \models \alpha[s] \\ &\iff \text{not } N \models \alpha[h_\ast s] \\ &\iff N \models \neg \alpha[h_\ast s]. \end{align*} For conjunction, \begin{align*} M \models (\alpha \wedge \beta)[s] &\iff M \models \alpha[s] \text{ and } M \models \beta[s] \\ &\iff N \models \alpha[h_\ast s] \text{ and } N \models \beta[h_\ast s] \\ &\iff N \models (\alpha \wedge \beta)[h_\ast s]. \end{align*} The same argument applies to $\vee$, $\to$, and $\leftrightarrow$ when these connectives are taken as primitive. If they are defined from $\neg$ and $\wedge$, the previous two cases already cover them. [/step]

[step:Use bijectivity of the isomorphism to handle quantifiers]Assume the assignment-level equivalence has been proved for a formula $\alpha$, and let $y \in \operatorname{Var}$ be a variable. We prove the equivalence for $\exists y\,\alpha$. First observe that for every $b \in |M|$, \begin{align*} h_\ast(s[y \mapsto b]) = (h_\ast s)[y \mapsto h(b)]. \end{align*} Therefore, by the induction hypothesis applied to $\alpha$ and the assignment $s[y \mapsto b]$, \begin{align*} M \models \alpha[s[y \mapsto b]] \iff N \models \alpha[(h_\ast s)[y \mapsto h(b)]]. \end{align*} Now, \begin{align*} M \models \exists y\,\alpha[s] &\iff \text{there exists } b \in |M| \text{ such that } M \models \alpha[s[y \mapsto b]] \\ &\iff \text{there exists } b \in |M| \text{ such that } N \models \alpha[(h_\ast s)[y \mapsto h(b)]]. \end{align*} Because $h: |M| \to |N|$ is surjective, the elements of the form $h(b)$ with $b \in |M|$ are exactly the elements of $|N|$. Hence \begin{align*} M \models \exists y\,\alpha[s] &\iff \text{there exists } c \in |N| \text{ such that } N \models \alpha[(h_\ast s)[y \mapsto c]] \\ &\iff N \models \exists y\,\alpha[h_\ast s]. \end{align*} For the universal quantifier, either repeat the same argument with “for every” in place of “there exists,” using bijectivity of $h$, or use the equivalence $\forall y\,\alpha \equiv \neg \exists y\,\neg \alpha$ together with the already established cases for negation and existential quantification. Thus the assignment-level equivalence holds for quantified formulas.[/step]

[guided]The quantifier step is the only place where surjectivity of the isomorphism is essential. For existential formulas, witnesses in $M$ must correspond exactly to witnesses in $N$. Assume the induction hypothesis holds for $\alpha$. Let $y$ be a variable. For $b \in |M|$, the assignment $s[y \mapsto b]$ sends $y$ to $b$ and otherwise agrees with $s$. Transporting this assignment through $h$ gives the assignment into $N$ that sends $y$ to $h(b)$ and otherwise agrees with $h_\ast s$: \begin{align*} h_\ast(s[y \mapsto b]) = (h_\ast s)[y \mapsto h(b)]. \end{align*} Therefore the induction hypothesis gives \begin{align*} M \models \alpha[s[y \mapsto b]] \iff N \models \alpha[(h_\ast s)[y \mapsto h(b)]]. \end{align*} Now unpack the meaning of the existential quantifier: \begin{align*} M \models \exists y\,\alpha[s] \end{align*} means that there is some $b \in |M|$ such that \begin{align*} M \models \alpha[s[y \mapsto b]]. \end{align*} Using the induction hypothesis, this is equivalent to saying that there is some $b \in |M|$ such that \begin{align*} N \models \alpha[(h_\ast s)[y \mapsto h(b)]]. \end{align*} Because $h$ is surjective, every element $c \in |N|$ has the form $c = h(b)$ for some $b \in |M|$. Thus the last condition is equivalent to \begin{align*} \text{there exists } c \in |N| \text{ such that } N \models \alpha[(h_\ast s)[y \mapsto c]]. \end{align*} This is exactly the definition of \begin{align*} N \models \exists y\,\alpha[h_\ast s]. \end{align*} The universal quantifier follows in the same way by replacing existential witnesses with arbitrary elements, or equivalently from \begin{align*} \forall y\,\alpha \equiv \neg \exists y\,\neg \alpha. \end{align*} Since negation and existential quantification have already been shown to be preserved, universal quantification is preserved as well.[/guided]

[step:Apply the assignment-level result to the given tuple] By structural induction on formulas, the preceding steps prove that for every $L$-formula $\psi$ and every assignment $s: \operatorname{Var} \to |M|$, \begin{align*} M \models \psi[s] \iff N \models \psi[h_\ast s]. \end{align*} Now choose an assignment $s: \operatorname{Var} \to |M|$ such that \begin{align*} s(x_i) = a_i \end{align*} for every $i \in \{1,\dots,n\}$. Since the free variables of $\varphi$ are contained in $\{x_1,\dots,x_n\}$, the truth value of $\varphi$ under $s$ depends only on the values $s(x_1),\dots,s(x_n)$. Also, \begin{align*} (h_\ast s)(x_i) = h(s(x_i)) = h(a_i) \end{align*} for every $i \in \{1,\dots,n\}$. Applying the assignment-level equivalence to $\psi := \varphi$ gives \begin{align*} M \models \varphi(a_1,\dots,a_n) \iff N \models \varphi(h(a_1),\dots,h(a_n)). \end{align*} This is the desired isomorphism invariance of first-order formulas. [/step]