I'm reading the paper "Weak Systems of Gandy, Jensen and Devlin" by Mathias.
The $\mathsf{ReS}$ consists of this: Extensionality, Null set, Pairing, Union, Set difference, $\Delta_0$ Separation, $\Pi_1$ Foundation. And double well-ordering is a linear ordering such that every non-empty subset has both a least and a greatest element. In $\mathsf{ZF}$, it is easy to show that "$x$ admits a double well-ordering" is equivalent to "$x$ is in bijection with some member in $\omega$". He shows that in fact it can be shown also in $\mathsf{ReS}$, which is weaker than $\mathsf{ZF}$, and it needs the $\Pi_1$ Foundation. For the $\implies$ part, his proof goes like this.
Let $X$ be a set with a double well-ordering $\le$. Let's say $f$ is an attempt at $x \in X$ if $\operatorname{dom}(f) = \{y \mid y \le x\}$ and for all $y \in \operatorname{dom}(f)$, $f(y) = \{f(z) \mid z < y\}$. This formula $\mathrm{Att}(f, x)$ can be easily written as a $\Delta_0$ formula. And then consider the class $\{x \mid x \in X \land \neg\exists f \mathrm{Att}(f, x)\}$. This class is $\Pi_1$. Let's assume that the class is not empty. Then there is a $\le$-least element $\bar{x} \in X$. $\ldots$
At this point he points out that the class is $\Pi_1$ and retrieves the least element. Let $A$ denote the class. Firstly, the definition of double well-ordering says every subset not subclass(otherwise there is no point in pointing out that $A$ is $\Pi_1$) so we can't directly get the least element of $A$. Secondly, we don't have $\Pi_1$ Separation so we don't know that $A$ is actually a set. Then how can we get the least element of $A$?
I think the proof should start like this: Let $x$ be an $\in$-minimal element of $A$. How can I proceed here?
Ok. This is an old question but I still have no idea. If we can form the transitive collapse of the $\Pi_1$ class, we can use $\Pi_1$ foundation to retrieve the least element. The so called attempt provides the transitive collapse of an initial segment. So if there exists an $x \not\in A$ which has an element of $A$ smaller than it, the argument holds. If not, $A$ is a tail segment of $X$. Again stuck here.