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.