Small elementary submodel meeting every definable equivalence class (source code)

= Small elementary submodel meeting every definable equivalence class

Let $N$ be uncountable and saturated, and let a formula define an equivalence relation. If every small elementary submodel of $N$ meets every class, then there are only finitely many classes. Otherwise a small elementary submodel $M$ yields the finitely satisfiable type $\{\neg E(x,m):m\in M\}$, contradicting saturation.