\documentclass[a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{a4wide}


\begin{document}
\noindent
We want to prove that $\mathcal I=\left<U,\cdot^\mathcal I\right>$ is a model of
\[\varphi = \forall x \exists y\,((\textup{f}(x) = c) \to \textup{P}(x, y)))\]
with
\begin{align*}
    &U = \{u_1, u_2\}\\
    &\textup{c}^{\mathcal I} = u_1\\
    &\textup{f}^{\mathcal I} = \{u_1 \mapsto u_2, u_2 \mapsto u_1\} \\
    &\textup{P}^{\mathcal I} = \{(u_2, u_2)\}
\end{align*}

\noindent
\textit{Proof:} Consider any variable assignment $\alpha$. We first
look at $\alpha_1 = \alpha[x := u_1][y := u_2]$.

Because $\textup{c}^{\mathcal I} = u_1$ and $\textup{f}(x)^{\mathcal I,
\alpha_1} = \textup{f}^{\mathcal I}(\alpha_1(x)) = \textup{f}^{\mathcal
I}(u_1) = u_2 \neq u_1 = \textup{c}^{\mathcal I}$, we have
\[\mathcal I, \alpha_1 \not\models (\textup{f}(x) = c) \text{ or }
  \mathcal I, \alpha_1 \models \lnot(\textup{f}(x) = c).\]
so we also know that
\[\mathcal I, \alpha_1 \models (\lnot(\textup{f}(x) = c) \lor \textup{P}(x, y))
  \text{ which means }
  \mathcal I, \alpha_1 \models ((\textup{f}(x) = c) \to \textup{P}(x, y)).\]
Since there is a $u \in U$ (namely $u_2$) such that $\mathcal I,
\alpha[x := u_1][y := u] \models ((\textup{f}(x) = c) \to \textup{P}(x,
y))$ we can use the definition of $\models$ for existentially quantified formulas to derive
\[\mathcal I, \alpha[x := u_1] \models \exists y\, ((\textup{f}(x) = c) \to \textup{P}(x, y)) \quad (*)\]

We now look at $\alpha_2 = \alpha[x:= u_2][y := u_2]$. Because
$(\alpha_2(x), \alpha_2(y)) = (u_2, u_2) \in \textup{P}^{\mathcal I}$,
we know that $\mathcal I, \alpha_2 \models \textup{P}(x, y)$ and (with
the same reasoning as above), we conclude that
\[\mathcal I, \alpha_2 \models ((\textup{f}(x) = c) \to \textup{P}(x, y)).\]
Since there is one $u\in U$ (namely  $u_2$) such that
$\mathcal I, \alpha[x := u_2][y := u] \models ((\textup{f}(x) = c) \to \textup{P}(x, y))$
we can use the definition of $\models$ for existentially quantified formulas to derive
\[\mathcal I, \alpha[x := u_2] \models \exists y\, ((\textup{f}(x) = c) \to \textup{P}(x, y)) \quad (**)\]

We have shown (in $(*)$ and $(**)$) that
$\mathcal I, \alpha[x := u] \models \exists y\, ((\textup{f}(x) = c) \to \textup{P}(x, y))$
holds for all $u \in U$, so we have
\[\mathcal I, \alpha \models \forall x \exists y\, ((\textup{f}(x) = c) \to \textup{P}(x, y))\]
which is what we wanted to show ($\mathcal I, \alpha \models \varphi$ for all variable assignments $\alpha$).

\end{document}
