Given a finite structure $\mathfrak{A}$ with Universe $|A| < \infty$ and signature $\tau$. We say a pair $(a,a') \in A$ satisfies a $\tau$-formular $\varphi$ iff
$$ \mathfrak{A} \models \varphi(a,a').$$
Additionally, we have an extension $\mathfrak{A}'$ of the structure $\mathfrak{A}$ which adds a strict ordering $<$ on $A$. Hence, we can express properties with $\tau \cup \{<\}$-formulas. But $\varphi$ does not depend on $<$.
We assume that there is at least one pair satisfying $\varphi$.
With the help of this ordering we want to make $\varphi$ unique. Hence, we are looking for a $\tau \cup \{<\}$-formula $\psi$ s.t. there is exactly one pair $(a,a') \in A$ with $\mathfrak{A}' \models \psi(a,a')$ and $(a,a')$ also satisfies $\varphi$.
Without the formalism: We have a property $\varphi$ (not dependent on the ordering) satisfied by several pairs. We want to select a unique pair by using a pre-existing ordering.
A natural solution is the lexicographically minimal pair $(a,a')$ which satisfies $\varphi$:
\begin{align*} \mathsf{lexmin}(\varphi,a,a') := & \varphi(a,a')\land \\ & \lnot \exists b,b' (a<b \land \varphi(b,b'))\land \\ & \lnot \exists b,b' (a=b \land a' < b' \land \varphi(b,b')\\ \end{align*}
I need this in a proof which requires me to use few axillary variables i.e. $b,b'$ in this context. Is it also possible to make the pair unique with just one auxiliary variable?