Collapse of elementary membership submodels

Elementary embeddings, substructures and chains: Let $\mathcal{A},\mathcal{M}$ be nonempty set structures for the same finite-arity set signature $L$. An elementary embedding is a function $e:A\to M$ such that, for every $L$-formula $\varphi$ and every tuple $\bar{a}$ assigning its finitely many free variables,

$\mathcal{A}\models \varphi [\bar{a}]⟺\mathcal{M}\models \varphi [e\bar{a}]\mathrm{.}$

Repeated parameters are allowed; a sentence uses the empty tuple. Tuple satisfaction means satisfaction by any full assignment extending that tuple, as justified by lem-satisfaction-coincidence. Applying the displayed condition to $x=y$ gives $a=b$ iff $e(a)=e(b)$, so $e$ is injective. Applying it to $x=c$, to $y=f(\bar{x})$, and to $R(\bar{x})$ shows that it preserves constants and functions and preserves and reflects relations.

A substructure $\mathcal{A}\subseteq \mathcal{M}$ has nonempty carrier $A\subseteq M$, contains all constant interpretations, is closed under every original function, and has the restricted functions and relations. It is elementary, written $\mathcal{A}\prec \mathcal{M}$, when its inclusion is an elementary embedding. An elementary chain indexed by an ordinal $\lambda$ is a set sequence $({\mathcal{M}}_{\alpha }{)}_{\alpha <\lambda }$ with ${\mathcal{M}}_{\alpha }\prec {\mathcal{M}}_{\beta }$ whenever $\alpha <\beta <\lambda$; no continuity at limit indices is required. The definition allows $\lambda =0$, but a union theorem must exclude it to ensure a nonempty carrier.

The structures are elementarily equivalent, written $\mathcal{A}\equiv \mathcal{M}$, when they agree on every $L$-sentence. This specifies no map. A sentence theory $T$ is categorical in cardinality $\kappa$ if any two models of $T$ with cardinality $\kappa$ are isomorphic. Existence of such models is a separate assertion; this convention allows vacuous categoricity, including cardinality zero since carriers are nonempty.

Conventions and prerequisites: def-set-structures-and-variable-assignments, def-theories-models-and-semantic-consequence.

Mostowski collapse for extensional relations: Every well-founded setlike extensional relation $R$ on a definable class $X$ is isomorphic to membership on a unique transitive definable class $Y$, by a unique definable isomorphism $\pi :X\to Y$. For a set domain $X$, the isomorphism and its image are sets. This holds without ambient Foundation.

Isomorphisms preserve satisfaction: For any homomorphism $h:\mathcal{M}\to \mathcal{N}$, term $t$ and assignment $s$, $\mathrm{⟦}t{\mathrm{⟧}}_{h\circ s}^{\mathcal{N}}=h(\mathrm{⟦}t{\mathrm{⟧}}_s^{\mathcal{M}})$. If $h$ is a surjective strong homomorphism, then $\mathcal{M},s\models \varphi$ iff $\mathcal{N},h\circ s\models \varphi$ for every equality-free formula $\varphi$. If $h$ is an isomorphism, the equivalence holds for all formulas, including equality.