Two measurable cardinals under an ultrapower embedding (source code)

= Two measurable cardinals under an ultrapower embedding

Let $\kappa_0<\kappa_1<\lambda$, where both $\kappa_i$ are measurable and $\lambda$ is inaccessible, and let $j_i:V_\lambda\to M_i$ be ultrapower embeddings by measures on $\kappa_i$. Then
$$
j_0(\kappa_1)=\kappa_1,
\qquad
j_1(\kappa_0)=\kappa_0.
$$
The second equality follows from the critical point. For the first, regularity gives continuity of $j_0$ at $\kappa_1$, while strong-limitness bounds $j_0(\beta)<\kappa_1$ for every $\beta<\kappa_1$.