[proofplan] We prove well-foundedness by contradiction. An infinite descending $\in_U$-chain in the ultrapower can be represented by a countable sequence of functions $f_n:I\to V$. The definition of $\in_U$ gives a countable family of $U$-large sets on which the pointwise membership relations hold. Countable completeness gives one index $i\in I$ where all of these pointwise relations hold simultaneously, producing an infinite descending membership chain in $V$, contradicting Foundation. [/proofplan] [step:Assume a descending ultrapower membership chain and choose representatives] Suppose, toward a contradiction, that $\in_U$ is not well-founded on $\operatorname{Ult}(V,U)$. Then there exists a sequence \begin{align*} x:\omega &\to \operatorname{Ult}(V,U) \end{align*} such that, writing $x_n:=x(n)$ for each $n\in\omega$, \begin{align*} x_{n+1}\in_U x_n \end{align*} for every $n\in\omega$. For each $n\in\omega$, choose a representative function \begin{align*} f_n:I &\to V \end{align*} such that $x_n=[f_n]_U$. Thus the assumed descending chain has the form \begin{align*} [f_{n+1}]_U\in_U[f_n]_U \end{align*} for every $n\in\omega$. [/step] [step:Translate the ultrapower relation into countably many pointwise membership conditions] For each $n\in\omega$, define the set \begin{align*} A_n:=\{i\in I:f_{n+1}(i)\in f_n(i)\}. \end{align*} By the definition of the ultrapower membership relation $\in_U$, the relation $[f_{n+1}]_U\in_U[f_n]_U$ is equivalent to $A_n\in U$. Hence \begin{align*} A_n\in U \end{align*} for every $n\in\omega$. [guided] The point of passing from the classes $[f_n]_U$ to the sets $A_n$ is that $\in_U$ is defined by membership holding on a $U$-large set of indices. For a fixed $n\in\omega$, the statement \begin{align*} [f_{n+1}]_U\in_U[f_n]_U \end{align*} means exactly \begin{align*} \{i\in I:f_{n+1}(i)\in f_n(i)\}\in U. \end{align*} We name this set \begin{align*} A_n:=\{i\in I:f_{n+1}(i)\in f_n(i)\}. \end{align*} Thus each $A_n$ records the indices where the $n$th membership relation in the ultrapower is witnessed pointwise. Since the descending chain assumption holds for every $n\in\omega$, we obtain a countable family $(A_n)_{n\in\omega}$ of members of the ultrafilter $U$. [/guided] [/step] [step:Use countable completeness to find one index satisfying all conditions] Since $U$ is countably complete and $A_n\in U$ for every $n\in\omega$, the countable intersection \begin{align*} A:=\bigcap_{n\in\omega}A_n \end{align*} belongs to $U$. Because $U$ is an ultrafilter, it is proper, so $\varnothing\notin U$. Therefore $A\ne\varnothing$. Choose an index $i_0\in A$. By the definition of $A$, for every $n\in\omega$ we have $i_0\in A_n$, hence \begin{align*} f_{n+1}(i_0)\in f_n(i_0). \end{align*} [/step] [step:Contradict Foundation with a descending membership chain in $V$] Define a sequence \begin{align*} y:\omega &\to V \end{align*} by \begin{align*} y(n):=f_n(i_0). \end{align*} The previous step gives \begin{align*} y(n+1)\in y(n) \end{align*} for every $n\in\omega$. Thus $V$ contains an infinite descending membership chain \begin{align*} y(0)\ni y(1)\ni y(2)\ni \cdots. \end{align*} This contradicts the Axiom of Foundation (citing a result not yet in the wiki: Foundation), which rules out such infinite descending $\in$-chains. Therefore no descending $\in_U$-sequence exists in $\operatorname{Ult}(V,U)$, so $\in_U$ is well-founded. [/step]