I have cross-posted this question on MO. This is the link:https://mathoverflow.net/questions/351894/lt-ip-is-a-well-defined-well-ordering-of-iterable-set-premice
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:
It kindly was pointed out to me at MO in the comments by Yair Hayut that the definition of $\lt_{ip}$ here is a little bit flawed. I fixed it.
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.
