Como he dicho en un comentario anterior, me imaginé cómo probar esto poco después de la publicación de mi pregunta. Ya no me gusta mi solución, he pospuesto responder a mi propia pregunta en la esperanza de que alguien ha publicado una más elegante respuesta primero. Ahora que parece poco probable, déjame arreglar este problema proporcionando un boceto:
La clave para mi prueba es la prueba de que el Principio de Reflejo (como se puede encontrar en Kunen de la Teoría de conjuntos libro, por ejemplo) -- la declaración solo no ayuda desde $\pi[\mathrm{Ord}]$ no puede contener una $N$definibles por el club (o de cualquier club, para el caso).
Primero vamos a suponer que $(M; \in) \models \mathrm{ZFC}^-$. Deje $\vec{x} \in M$ $\phi$ ser tal que $(M; \in) \models \phi[\vec{x}]$. Arreglar tu favorito $M$-definible, monotono, cofinal secuencia $(M_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$ tal que $\phi$ y todos sus subformulae son absolutos entre el $M$ y todos los $M_\alpha$ $(\dagger)$. Para $\alpha \in M \cap \mathrm{Ord}$ deje $N_\alpha = \pi(M_{\alpha}$). Lo que me desconcertó al principio, es que el$(N_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$, en general, no inherente a todos los lindos propiedades adicionales de la $M_\alpha$-secuencia, pero sin duda sigue siendo monotono, cofinal y, para todos los $\alpha$ y todos los $\vec{y} \in M_{\alpha}$ hemos
$$
\begin{align*}
(M; \in) \models \phi[\vec{y}] & \iff (M_{\alpha}; \in) \models \phi[\vec{y}] \\
& \iff (N_{\alpha}; \in) \models \phi[\pi(\vec{y})].
\end{align*}
$$
Ahora uso este para concluir, a través de una inducción sobre la complejidad de $\phi$,$(N; \in) \models \phi[\pi(\vec{x})]$.
Si, por otro lado, $(N; \in) \models \mathrm{ZFC}^-$, básicamente la misma prueba en obras $(\ddagger)$. Este tiempo de empezar con un $N$-definible, monotono, cofinal secuencia $(N_\alpha \mid \alpha \cap N \cap \mathrm{Ord})$ de los transitivos conjuntos tales que a $\phi$ y todos sus subformulae son absoluta entre todos los $N_\alpha$ $N$ y considerar la posibilidad de que el pullback
$$
(\pi^{-1}[N_{\alpha}] \mid \alpha \N \cap \mathrm{Ord}).
$$
Esta secuencia, en mi mente, se ve aún más desagradable que el de antes, pero por suerte conseguimos que todavía se compone de conjuntos transitivos $(\Diamond)$ (lo que ayudará a lidiar con delimitada fórmulas) que combinados son cofinal en $M$ y todavía podemos obtener, por $\alpha \in N \cap \mathrm{Ord}$ $\vec{y} \in \pi^{-1}[N_{\alpha}]$ que
$$
\begin{align*}
(\pi^{-1}[N_\alpha]; \in) \models \phi[\vec{y}]
& \iff (N_{\alpha}; \in) \models \phi[\vec{y}] \\
& \iff (N; \in) \models \phi[\vec{y}].
\end{align*}
$$
Una similar en la inducción como antes, a continuación, finaliza la prueba.
$(\dagger)$ Esto existe por el Principio de Reflejo-que es comprobable en $\mathrm{ZFC}^-$ - y podríamos, si quisiéramos, imponer más requisitos de esta secuencia (por ejemplo, elegir ser continua o a ser un club-subsequece de $(V_\alpha^M \mid \alpha \in M \cap \mathrm{Ord}$).
$(\ddagger)$ Le gustaría tener un cofinal secuencia $(M_{\alpha} \mid \alpha \in M \cap \mathrm{Ord})$ tal que $(\pi(M_{\alpha}) \mid \alpha \in M \cap \mathrm{Ord})$ es monotono, continua, cofinal y $N$-definibles para aplicar el Principio de Reflejo y tire de la declaración de la espalda a través de $\pi$. Pero no podemos-no, incluso si supiéramos que $(M; \in) \models \mathrm{ZFC}^-$.
$(\Diamond)$ A ver que ellos son transitivos, parece más fácil mirar a $(\pi[M]; \in)$ $\Sigma_0$- subestructura de $(N; \in)$ e ver $\pi$ como el colapso de Mostowski. A continuación, $N_\alpha \cap \pi[M]$ se derrumba para el conjunto transitivo $\pi^{-1}[N_\alpha]$.
