[proofplan]
Starting from a non-principal $\kappa$-complete ultrafilter $U$ on $\kappa$, we form the ultrapower $\operatorname{Ult}(V,U)$ and use Łoś's theorem to obtain an elementary ultrapower embedding. Since $U$ is countably complete, the ultrapower is well-founded, so the Mostowski collapse gives a transitive class target. The critical point is computed by showing that all ordinals below $\kappa$ are fixed while $\kappa$ is moved. Conversely, from an elementary embedding $j:V\to M$ with critical point $\kappa$, we derive the ultrafilter $U_j=\{X\subset\kappa:\kappa\in j(X)\}$ and verify directly that it is non-principal and $\kappa$-complete.
[/proofplan]
[step:Build the ultrapower from a measurable cardinal]
Assume $\kappa$ is measurable. Let $U$ be a non-principal $\kappa$-complete ultrafilter on $\kappa$.
Define the class ultrapower [equivalence relation](/page/Equivalence%20Relation) on functions $f:\kappa\to V$ by
\begin{align*}
f \sim_U g \iff \{\alpha\in\kappa : f(\alpha)=g(\alpha)\}\in U.
\end{align*}
Let $[f]_U$ denote the equivalence class of $f:\kappa\to V$, and let $\operatorname{Ult}(V,U)$ be the class of all such equivalence classes. Define the ultrapower membership relation $\in_U$ on $\operatorname{Ult}(V,U)$ by
\begin{align*}
[f]_U \in_U [g]_U \iff \{\alpha\in\kappa : f(\alpha)\in g(\alpha)\}\in U.
\end{align*}
Define the ultrapower embedding
\begin{align*}
j_U:V &\to \operatorname{Ult}(V,U)
\end{align*}
\begin{align*}
x &\mapsto [c_x]_U,
\end{align*}
where $c_x:\kappa\to V$ is the constant function with value $x$.
By Łoś's theorem for ultrapowers, applied to the ultrafilter $U$ and the structure $(V,\in)$, the map $j_U$ is elementary. Since $U$ is $\kappa$-complete and $\kappa$ is uncountable, $U$ is countably complete. Therefore the well-foundedness theorem for countably complete ultrapowers implies that $(\operatorname{Ult}(V,U),\in_U)$ is well-founded. By the Mostowski collapse theorem, there is a transitive class $M$ and an isomorphism
\begin{align*}
\pi:\operatorname{Ult}(V,U)&\to M.
\end{align*}
Define
\begin{align*}
j:V&\to M
\end{align*}
\begin{align*}
x&\mapsto \pi(j_U(x)).
\end{align*}
Because $j_U$ is elementary and $\pi$ is an isomorphism of membership structures, $j$ is elementary.
[guided]
We start from the object supplied by measurability: a non-principal $\kappa$-complete ultrafilter $U$ on $\kappa$. The standard way to turn such a measure into an elementary embedding is to form the ultrapower of the universe by $U$.
For functions $f,g:\kappa\to V$, define
\begin{align*}
f \sim_U g \iff \{\alpha\in\kappa : f(\alpha)=g(\alpha)\}\in U.
\end{align*}
This says that two functions are identified when they agree on a $U$-large subset of $\kappa$. We write $[f]_U$ for the equivalence class of $f$, and we define $\operatorname{Ult}(V,U)$ to be the class of all such equivalence classes.
The membership relation in the ultrapower must also be interpreted $U$-almost everywhere. Thus we define
\begin{align*}
[f]_U \in_U [g]_U \iff \{\alpha\in\kappa : f(\alpha)\in g(\alpha)\}\in U.
\end{align*}
This is well-defined because changing $f$ or $g$ on a $U$-small set does not change whether the displayed set belongs to the ultrafilter.
Now define the ultrapower embedding
\begin{align*}
j_U:V &\to \operatorname{Ult}(V,U)
\end{align*}
\begin{align*}
x &\mapsto [c_x]_U,
\end{align*}
where $c_x:\kappa\to V$ is the constant function with value $x$. This map sends each set to the equivalence class of the constant function representing it.
Łoś's theorem for ultrapowers states that first-order formulas are true in the ultrapower exactly when they are true on a $U$-large set of indices. Applied to the structure $(V,\in)$, this gives that $j_U$ is elementary. The theorem used here is not yet linked in the wiki: Łoś's theorem for ultrapowers.
The target of $j_U$ is initially only an ultrapower structure, not necessarily a transitive class. We need transitivity for the theorem statement. Since $U$ is $\kappa$-complete and $\kappa$ is uncountable, $U$ is countably complete. The standard well-foundedness theorem for countably complete ultrapowers then implies that $(\operatorname{Ult}(V,U),\in_U)$ is well-founded. This theorem is also not yet linked in the wiki: well-foundedness of countably complete ultrapowers.
Because the ultrapower is well-founded and extensional, the Mostowski collapse theorem applies. It gives a transitive class $M$ and an isomorphism
\begin{align*}
\pi:\operatorname{Ult}(V,U)&\to M.
\end{align*}
Finally define
\begin{align*}
j:V&\to M
\end{align*}
\begin{align*}
x&\mapsto \pi(j_U(x)).
\end{align*}
The map $j$ is elementary because it is the composition of the elementary map $j_U$ with the collapse isomorphism $\pi$.
[/guided]
[/step]
[step:Compute the critical point of the ultrapower embedding]
We show that $\operatorname{crit}(j)=\kappa$. It suffices to compute this before the collapse, because $\pi$ preserves the membership structure and hence preserves the ordinal comparison inside the collapsed ultrapower.
Let $\alpha<\kappa$ be an ordinal. For every function $f:\kappa\to\alpha$, the family of fibers
\begin{align*}
A_\beta=\{\xi\in\kappa:f(\xi)=\beta\},\qquad \beta<\alpha,
\end{align*}
is a partition of $\kappa$ into fewer than $\kappa$ many sets. Since $U$ is a $\kappa$-complete ultrafilter, exactly one fiber $A_\beta$ belongs to $U$. Therefore $[f]_U=[c_\beta]_U$. Hence every element of the ultrapower ordinal $j_U(\alpha)$ is represented by a constant function with value below $\alpha$, so $j_U(\alpha)=\alpha$. After the collapse, $j(\alpha)=\alpha$ for every $\alpha<\kappa$.
Now let
\begin{align*}
\operatorname{id}_\kappa:\kappa&\to\kappa
\end{align*}
\begin{align*}
\xi&\mapsto \xi
\end{align*}
be the identity function on $\kappa$. For every $\alpha<\kappa$, we have
\begin{align*}
\{\xi\in\kappa:\alpha<\xi\}\in U,
\end{align*}
because its complement $\alpha+1$ has cardinality less than $\kappa$ and $U$ is non-principal and $\kappa$-complete. Hence
\begin{align*}
[c_\alpha]_U \in_U [\operatorname{id}_\kappa]_U.
\end{align*}
Also
\begin{align*}
[\operatorname{id}_\kappa]_U \in_U [c_\kappa]_U=j_U(\kappa),
\end{align*}
because $\operatorname{id}_\kappa(\xi)=\xi\in\kappa$ for all $\xi<\kappa$. Thus $j_U(\kappa)$ strictly contains all ordinals below $\kappa$ and contains the additional element $[\operatorname{id}_\kappa]_U$, so $j_U(\kappa)>\kappa$. Therefore $j(\kappa)>\kappa$ after the collapse, while every ordinal below $\kappa$ is fixed. Hence $\operatorname{crit}(j)=\kappa$, and $j$ is nontrivial.
[/step]
[step:Derive an ultrafilter from an elementary embedding]
Conversely, assume there are a transitive class $M$ and a nontrivial elementary embedding $j:V\to M$ with $\operatorname{crit}(j)=\kappa$.
Define
\begin{align*}
U_j=\{X\subset\kappa:\kappa\in j(X)\}.
\end{align*}
We prove that $U_j$ is a non-principal $\kappa$-complete ultrafilter on $\kappa$.
First, $U_j$ is an ultrafilter. Let $X\subset\kappa$. Since $j$ is elementary,
\begin{align*}
j(\kappa\setminus X)=j(\kappa)\setminus j(X).
\end{align*}
Because $\operatorname{crit}(j)=\kappa$, we have $j(\kappa)>\kappa$, and since $M$ is transitive, the statement $\kappa\in j(\kappa)$ is interpreted correctly in $M$. Thus exactly one of $\kappa\in j(X)$ and $\kappa\in j(\kappa\setminus X)$ holds. Hence exactly one of $X$ and $\kappa\setminus X$ belongs to $U_j$.
If $X,Y\subset\kappa$ and $X\subset Y$ with $X\in U_j$, then $j(X)\subset j(Y)$ by elementarity, so $\kappa\in j(Y)$ and $Y\in U_j$. If $X,Y\in U_j$, then $\kappa\in j(X)$ and $\kappa\in j(Y)$, so
\begin{align*}
\kappa\in j(X)\cap j(Y)=j(X\cap Y),
\end{align*}
and hence $X\cap Y\in U_j$. Therefore $U_j$ is a filter, and the complement property above makes it an ultrafilter.
[/step]
[step:Verify non-principality and $\kappa$-completeness of the derived ultrafilter]
For non-principality, let $\alpha<\kappa$. Since $\operatorname{crit}(j)=\kappa$, $j(\alpha)=\alpha$, and therefore
\begin{align*}
j(\{\alpha\})=\{\alpha\}.
\end{align*}
Since $\kappa\ne\alpha$, we have $\kappa\notin j(\{\alpha\})$, so $\{\alpha\}\notin U_j$. Thus $U_j$ is non-principal.
Now let $\lambda<\kappa$, and let
\begin{align*}
\vec{X}:\lambda&\to \mathcal{P}(\kappa)
\end{align*}
\begin{align*}
i&\mapsto X_i
\end{align*}
be a sequence such that $X_i\in U_j$ for every $i<\lambda$. Since $\lambda<\kappa=\operatorname{crit}(j)$, we have $j(\lambda)=\lambda$, and elementarity gives
\begin{align*}
j(\vec{X})=\langle j(X_i):i<\lambda\rangle.
\end{align*}
For every $i<\lambda$, the assumption $X_i\in U_j$ means $\kappa\in j(X_i)$. Hence
\begin{align*}
\kappa\in \bigcap_{i<\lambda} j(X_i).
\end{align*}
By elementarity applied to the intersection operation on the sequence $\vec{X}$,
\begin{align*}
j\left(\bigcap_{i<\lambda}X_i\right)=\bigcap_{i<\lambda}j(X_i).
\end{align*}
Therefore
\begin{align*}
\kappa\in j\left(\bigcap_{i<\lambda}X_i\right),
\end{align*}
so
\begin{align*}
\bigcap_{i<\lambda}X_i\in U_j.
\end{align*}
Thus $U_j$ is $\kappa$-complete.
We have constructed a non-principal $\kappa$-complete ultrafilter on $\kappa$, so $\kappa$ is measurable. This proves the converse implication and completes the equivalence.
[/step]
