Elementary chains and compatible collapses

Let $\lambda >0$ and $U={\bigcup }_{\alpha <\lambda }{M}_{\alpha }$. F1 gives a set structure with $M_{\alpha }\prec U$. It satisfies Extensionality because any one stage does and sentences transfer by elementarity. Apply F2 with $X=M=U$ to obtain its collapse $\pi :U\to \bar{U}$, and similarly obtain ${\pi }_{\alpha }:M_{\alpha }\to {\bar{M}}_{\alpha }$ for each stage. Their uniqueness permits Replacement to collect these maps.

Define $j_{\alpha \beta }={\pi }_{\beta }\circ {\iota }_{\alpha \beta }\circ {\pi }_{\alpha }^{-1}$ and $j_{\alpha }=\pi \circ {\iota }_{\alpha }\circ {\pi }_{\alpha }^{-1}$. The inverse and forward collapses are isomorphisms and the inclusions are elementary, so each composite is elementary by the satisfaction equivalences. Its codomain is the corresponding transitive collapse, not the original carrier.

For $\alpha \le \beta \le \gamma$, cancellation gives $j_{\beta \gamma }{j}_{\alpha \beta }={\pi }_{\gamma }{\iota }_{\beta \gamma }({\pi }_{\beta }^{-1}{\pi }_{\beta }){\iota }_{\alpha \beta }{\pi }_{\alpha }^{-1}=j_{\alpha \gamma }$. The same calculation gives $j_{\beta }{j}_{\alpha \beta }=j_{\alpha }$, and $j_{\alpha \alpha }$ is the identity. This proves coherence without identifying any composite with a literal inclusion.