$\lt_{ip}$ is a well-defined well-ordering of iterable set premice

Question

I am cross-posting this question from MSE, where I asked it about $3$ months ago and I decided to ask it here as well.

---

This question of mine arises from Kanamori's the higher infinite, where he tries to prove the result attributed to Silver and Solovay, that if $\omega_1^{L[U]} = \omega_1$, then there is a $\Pi_2^1$ set without the perfect set property.

---

Here we are dealing with ZFC$^-$(ZFC minus the Powerset Axiom) premice.

To be more precise, assume that $M$ is a transitive model of ZFC$^-$ and that $U$ is some set in $V$. We say that $\langle M, \in, U\rangle$ is a ZFC$^-$ premouse (at $\kappa$) iff $U$ is an $M$-ultrafilter over $\kappa$ and that for some $\zeta$, $M = L_\zeta[U].$

Also we say that two premice $\langle M, \in, U\rangle$ and $\langle N, \in, W\rangle$ are comparable iff $\exists F \exists \zeta \exists \eta$ such that $M = L_\zeta[F]$ and that $N = L_\eta[F]$.

Now there is a lemma (called the Comparison lemma) which states that:

If $\langle M, \in, U\rangle$ and $\langle N, \in, W\rangle$ are iterable premice, then they have iterates which are comparable.

Now let $\langle M, \in, U\rangle$ and $\langle N, \in, W\rangle$ be iterable premice, define $\lt_{ip}$ in the following manner:

$\langle M, \in, U\rangle \lt_{ip}\langle N, \in, W\rangle$ iff there exists some $F$ and some $\zeta$ and $\eta$ such that $\langle L_\zeta[F], \in, F\cap L_\zeta[F]\rangle$ is an iterate of $\langle M, \in, U\rangle$ and $\langle L_\eta[F], \in, F\cap L_\eta[F]\rangle$ is an iterate of $\langle N, \in, W\rangle$, such that $\zeta \lt \eta$.

Now Kanamori says that this ordering is a well-defined well-ordering of iterable set premice. And he says that this is straightforward to check, using the comparison lemma.

---

I am still stuck on showing that this is well-defined. The best idea I had was to show that: if $\alpha$ and $\beta$ are the first indices of the iterations of $M$ and $N$ which are comparable, then all the higher iterates should be comparable in a "coherent" fashion.

So what I did was this: Let $\langle M_\alpha, \in, U_\alpha, \kappa_\alpha, i_{\alpha\beta} \rangle_{\alpha\le\beta\in\text{On}}$ and $\langle N_\alpha, \in, W_\alpha, \lambda_\alpha, j_{\alpha\beta} \rangle_{\alpha\le\beta\in\text{On}}$ be the iterations of $M$ and $N$, respectively. Then let $\alpha$ and $\beta$ be the first ordinals where $M_\alpha$ and $N_\beta$ are comparable. Let $F, \zeta, \eta$ be such that: $M_\alpha = L_\zeta[F]$ and $N_\beta = L_\eta[F]$. There are $2$ cases:

$(1)$ $\zeta = \eta$: At this point I know that the rest of their iterations should be the same. But I think for totality's sake I have to show that $M = N$. Which is not obvious to me at the moment. (*)

$(2)$ $\zeta \lt \eta$: We can see that $M_\alpha,U_\alpha \in N_\beta$ so that the iteration of $N$ can witness the iteration of $M$ inside it. So for $\delta \in \text{On}$, we can see that $M_{\alpha + \delta} \in N_{\beta + \delta}$, but I can't generalize this argument for all $\delta \ge \alpha$ and $\xi \ge \beta$, i.e. that if $M_\delta$ and $N_\xi$ are comparable via some $G$, then $M_\delta$ falls below $N_\xi$.(**)

(*) and (**) are the two points where I can't finish this argument. Now my question is that, can the above argument be completed? Or is there some other way to prove that $\lt_{ip}$ is well-defined?

Also I would really appreciate any hints or remarks concerning the well-order part.

---

EDIT I:

The material here can be found in Kanamori's "The Higher Infinite", page $273$, $2$nd edition.

---

EDIT II: As Yair Hayut kindly pointed out in the comments below, my definition of $\lt_{ip}$ was flawed. It is now fixed.

Also it was pointed out that it is reasonable to identify each premouse with it's iterates. In this light $(1)$ becomes:

$(1)^*$ In the case $\zeta = \eta$ we should find some premouse $\langle B, \in, O\rangle$ such that both $M$ and $N$ are iterates of $B$. In this case we insure totality.

---

EDIT III:

Also $(1)^*$ is evidently equivalent to:

$(1)^+$ We have to show that one of $M$ or $N$ is an iterate of the other one.

Answer 1

Note that in those types of mice, the comparison process is simple:

Lemma: Let $M = L_{\alpha}[U]$, $N = L_{\beta}[W]$ be two mice. Let $\mu$ be a regular cardinal $\mu \geq (\max(\alpha,\beta))^+$. Then $M_{\mu} = L_{\alpha'}[F], N_{\mu} = L_{\beta'}[F]$ where $F$ is the club filter on $\mu$, $M_{\mu}$ is the iteration of $M$ for $\mu$ many steps and $N_\mu$ is the iteration of $N$ for $\mu$ many steps.

Proof: Let $C_M = \{\kappa_{\alpha} \mid \alpha < \mu\}$ be the critical points of the iteration on $M$. Then $C_M$ is a club at $\mu$, and $j_{\mu}(\kappa) = \mu$.

Moreover for all $X \in M_{\mu}$, $$X \in j_{\mu}(U)\iff \exists \zeta < \mu,\ X = j_{\zeta, \mu}(X'), \text{ and } X' \in j_{\zeta}(U)$$ In turn, this is equivalent to $$\forall\zeta' \geq \zeta,\ \kappa_{\zeta'} \in X.$$ On the other hand, if $X \notin j_{\mu}(X)$ then $j_{\mu}(\kappa) \setminus X \in j_{\mu}(U)$ and thus $X$ is disjoint from a club. We conclude that $M_\mu = L_{\alpha'}[F]$ for some ordinal $\alpha'$. The same argument works for $N$.

Lemma: Let $M, N, \alpha', \beta'$ be as above. $M<_{ip} N$ iff $\alpha' < \beta'$.

Proof: First, the order of $\alpha', \beta'$ does not depend on the choice of $\mu$. Moreover, if there is some iteration $M_{\xi}, N_{\eta}$ of different lengths such that $M_{\xi}$ is an initial segment of $N_{\eta}$ than continue by iterating both $M_{\xi}, N_{\eta}$ by $\mu$ many steps where $\mu$ is regular cardinal above the size of both $M_{\xi}, N_{\eta}$. Then by the previous lemma, $M_{\xi + \mu} = M_{\mu}$ is either an initial segment of $N_{\eta + \mu}$ or the other way. The second case cannot occur, since $M_{\xi}$ is an initial segment of $N_{\eta}$ and this is preserved by the longer iteration.