(Note that I'm considering extenders within the full context of $\mathsf{ZFC}$ rather than various fragments.)
For $E$ a $(\kappa,\lambda)$-extender, the well-foundedness of the limit ultrapower $\mathrm{ult}(V,E)$ is equivalent to countable completeness:
for every sequence $\langle a_n, X_n:n\in\omega\rangle$ with $X_n\in E_{a_n}$, there is a function $g:\bigcup_{n<\omega}a_n\rightarrow\kappa$ such that $g\mathord{"}a_n\in X_n$ for each $n<\omega$.
I'm able to show the supposedly harder direction that well-foundedness implies countable completeness (analogous to the proof for ultrafilters). But for some reason, I'm having trouble showing that countable completeness implies well-foundedness.
My initial idea was just to take a $\in^{\mathrm{ult}(V,E)}$-decreasing sequence $\langle[b_n,f_n]:n\in\omega\rangle$, and work with $a_n=\bigcup_{i\le n}b_n$ and just define $X_n$ by
$$t\in X_n\quad\text{iff}\quad\bigwedge_{i<n}f_{i+1}(t)\in f_{i}(t)\text{.}$$
From here we get a $g$ as above so that one consequence is $f_{n+1}(g\mathord{"}a_n)\in f_n(g\mathord{"}a_n)$. But this doesn't quite give what we want, which is that $f_{n+1}(g\mathord{"}a_{n+1})\in f_n(g\mathord{"}a_n)$ (and then consider $\langle f_n(g\mathord{"}a_n):n\in\omega\rangle$, contradicting the well-foundedness of $V$). So how are we supposed to relate $f_{n+1}(g\mathord{"}a_n)$ and $f_{n+1}(g\mathord{"}a_{n+1})$?
Perhaps I'm having tunnel-vision with this, but this is supposed to be the easier direction, given by a straightforward argument. Is there something I'm missing?
Best Answer
Okay, so if we assume that $g$ is order preserving, this isn't that difficult. I'm still not sure how to prove the result without this additional assumption, but some resources do have $g$ as order preserving.
Now when removing the dummy variables (or introducing them), I'll write the relevant function as $\mathrm{proj}_{a,b}$, defined by $\mathrm{proj}_{a,b}(a)=b$ and $\mathrm{proj}_{a,b}(\{\xi_0,\cdots,\xi_{|a|}\})=\{\xi_{i_0},\cdots,\xi_{i_m}\}$ when $\xi_0<\cdots<\xi_{|a|}$.
From here, as in the question, take $a_n=\bigcup_{i\le n}b_n$ and $t\in X_n$ iff (writing the transformed versions this time for clarity) $$ \bigwedge_{i<n} f_{i+1}^{b_{i+1},a_n}(t)\in f_i^{b_i,a_n}(t)\text{.}$$ Thus $X_n\in E_{a_n}$ by Łoś's theorem, and so we get an order preserving $g$ where $g\mathord{"}s_n\in X_n$. Because $g$ is order preserving, removing the dummy variables yields that for $i\le n$, $\mathrm{proj}_{a_n,b_i}(g\mathord{"}a_n)=g\mathord{"}b_i$. In particular, $f^{a_n,b_i}_{i}(g\mathord{"}a_n)=f_i(\mathrm{proj}_{a_n,b_i}(g\mathord{"}a_n))=f_i(g\mathord{"}b_i)$. And from here we can finally conclude that $\langle f_i(g\mathord{"}b_i):i\in\omega\rangle$ is a $\in$-decreasing sequence, contradicting well-foundedness.