As I found some problems in my writing and proof, I have heavily edited my questions.
So I am reading this corollary in Steel's notes, found here, and I am confusing myself over and over again. I hope someone can clarify the situation for me. First some context:
When I say $\omega$-complete ultrafilter, I mean that the intersection of countable sequences of members of that ultrafilter are nonempty. And we may assume that in $\mathsf{ZFC}$, we have linear iterability for normal ultrafilters. Also whenever $M \models \mathsf{ZFC} + `` \mathcal{E} \mbox{ is a family of normal ultrafilters''}$ and $I = \langle U_\alpha: \alpha \lt \lambda\rangle$ is an iteration of $(M, \mathcal{E})$, then $M^I_\infty$ denotes the direct limit of $I$ and $i_{\alpha\infty}$ denote the direct limit embeddings.
Now this is corollary $2.8$ of the above notes, together with the following exercise:
Corollary $2.8.$ Let $M \models \mathsf{ZFC} + `` \mathcal{E} \mbox{ is a family of normal ultrafilters''}$, with $M$ transitive, and $\omega_1 \in M$. Then $(M, \mathcal{E})$ is linearly iterable.
Proof. Working inside $M$, construct a $``\mbox{universal''}$ linear iteration $I = \langle U_\alpha: \alpha \lt \lambda\rangle$ with $(a)$ $\operatorname{cof}(\lambda) = \omega$, and $(b)$ whenever $W \in i_{0\alpha}(\mathcal{E})$, then $i_{\alpha\beta}(W) = U_\beta$ for cofinally many $\beta$. This implies that every $W \in i_{0\infty}(\mathcal{E})$ is $\omega$-complete. Thus $(M^I_\infty, i_{0\infty}(\mathcal{E}))$ is linearly iterable in $V$. Since $i_{0\infty}:M\rightarrow M^I_\infty$, $(M, \mathcal{E})$ is linearly iterable in $V$. $\Box$
Exercise. Prove that every $W \in i_{0\infty}(\mathcal{E})$ is $\omega$-complete, granted $(a)$ and $(b)$.
Questions:
Now I have partially worked my way through the corollary and have constructed an $I$ with some difference to what is suggested and I think I do understand what's going on, except for the questions I have below:
Firstly, I can only complete the proof with the crucial assumption that $M^I_\infty$ is actually well-founded in $V$. But I don't see how we can show this. It is well-founded from $M$'s perspective, but $V$ may not agree. So what can we say about this?
Secondly, I have proved the exercise but with one key difference. When building $I$, I made sure that $\operatorname{cof}(\lambda) = \omega_1$, instead of the suggested $\omega$! That's because when looking at our sequences from $^\omega W$ like $\langle A_n: n \in \omega \rangle$, we can bound their representatives given by $(b)$ in the iteration and then find some $\langle B_n: n\in\omega\rangle$ and $\alpha$, such that $i_{\alpha\infty}(B_n)=A_n$ and $B_n \in U_\alpha$ for each $n$. Then by normality we would have $i_{0\alpha}(\kappa) \in i_{\alpha{\alpha+1}}(B_n)$ for each $n$ and then we would have $i_{{\alpha+1}\infty}(i_{0\alpha}(\kappa))\in A_n$ for every $n$; and so $i_{{\alpha+1}\infty}(i_{0\alpha}(\kappa))\in \bigcap_n A_n$.
And as you can see from the above proof, I think $\operatorname{cof}(\lambda) = \omega$ is probably a typo right? Also the thing I have written is the only way I can think of that we can use the hypothesis $\omega_1\in M$.
I would really appreciate any thoughts and help, so I can make some progress. Also, sorry for the long post.
After consulting with a friend on twitter, we came to the following conclusion for the first question:
As $M \models \mathsf{ZFC}$, then each ultrapower is contained within $M$ by the virtue of $M \models \mathsf{Powerset}$. And in general, models of $\mathsf{ZFC}$ trap all iterations in themselves(unless of course when the length of the iteration is $\ge \operatorname{Ord}^M$). And since $I$ is iterated in $M$, $M$ can see $M^I_\infty$ as a subclass! At which point it must be well-founded.
This solves most of my confusion. I would still welcome any confirmation about my second question.