I'm looking for a proof that a type realised in a finite structure, modelling some theory $T$, is isolated (aka principal). Definitions for clarity are:
Definition An $n$-type $p$ is realised in a structure $\mathcal A$ with domain $A$ if and only if there are $a_1, \dots, a_n \in A$ such that $p \subseteq tp_{\mathcal A} (a_1 \dots a_n) = \{\phi \mid {\mathcal A} \vDash \phi(a_1 \dots a_n) \}$.
Definition An $n$-type $p$ is isolated (or principal) if and only if there is a formula $\psi$ in $n$ variables such that $T \vDash \exists v_1 \dots v_n \psi (v_1 \dots v_n )$ and for all formulae $\chi$ in $p$, we have $T \vDash \forall v_1 \dots v_n (\psi (v_1 \dots v_n ) \rightarrow \chi (v_1 \dots v_n ))$
Well let $(a_1 \dots a_n)$ be the tuple realising $p$ in $\mathcal A$.
I think that $T$, as a theory, may be assumed complete, and so if $|A|=N$, then the sentence $\exists v_1 \dots v_N ((\bigwedge_{i \neq j} v_i \neq v_j) \wedge \forall v \bigvee_{i} v=v_i) $ ensures all other models of $T$ are of the same cardinality as $T$?
Then finding a minimal set definable in $\mathcal A$ containing $(a_1 \dots a_n)$, the formula defining this set is exactly what we want? And such a minimal set may be found as $|B|=N<\infty \implies |B^n|<\infty \implies |{\mathcal P}(B^n)| < \infty$ for $B$ the domain of any model ${\mathcal B} \vDash T$, so the subset of definable sets containing $(a_1 \dots a_n)$ in ${\mathcal A}$ is finite as the set of definable sets is a subset of ${\mathcal P}(A^n)$. Taking the intersection of this finite subset gives the minimal definable subset containing $(a_1 \dots a_n)$.
Does this seem like a neat and correct argument?