The ordered Mostowski model

The order relation is fixed by every order automorphism, so it has empty support. We first verify the finite-support intersection fact used below. If $E_1,E_2\subseteq A$ are finite and $E=E_1\cap E_2$, then \operatorname{fix}(E)=\langle\operatorname{fix}(E_1)\cup\operatorname{fix}(E_2)\rangle. \tag{*} Indeed, cut $A$ at the points of $E$. In each resulting open interval the two finite sets $E_1\setminus E$ and $E_2\setminus E$ are disjoint. List their points and the images of those points under a given $\pi \in \mathrm{fix}(E)$. Move the image points into their required successive cuts, one at a time. To cross a point of $E_1\setminus E$, use an increasing finite partial bijection which fixes $E_2$; to cross a point of $E_2\setminus E$, use one which fixes $E_1$. The point being crossed is not in the fixed set, and density and the absence of endpoints provide a fresh point on the required side. Each such finite increasing partial bijection extends, by the usual interval-by-interval back-and-forth for a countable dense order without endpoints, to an automorphism in the indicated pointwise stabilizer. There are only finitely many marked and image points, so after finitely many moves the residual automorphism fixes $E_1$ (and the last correction may be taken to fix $E_2$). This proves $(\ast )$ on each component; joining the component automorphisms proves it on $A$. If $E_1,E_2$ support $x$, every factor on the right of $(\ast )$ fixes $x$. Thus every element of $\mathrm{fix}(E)$ fixes $x$, and $E_1\cap E_2$ supports $x$.

All supports contained in one fixed finite support form a finite family. Repeated intersection therefore gives a support $E_x$ contained in every support; it is the unique least support. Conjugating shows $g{E}_x$ is the least support of $gx$, so the least-support assignment is itself symmetric.

Suppose a well-order $◃$ of $A$ belonged to the model, and let $E$ be a finite support for it. The nonempty set $A\setminus E$ has a $◃$-least element $a$. It lies in one of the open intervals cut out by $E$; choose $b\mathrm{\ne }a$ in that interval. The finite increasing partial map fixing $E$ and sending $a$ to $b$ extends by back-and-forth to an order automorphism $\pi \in \mathrm{fix}(E)$. Because $E$ supports $◃$, $\pi$ preserves $◃$ and maps $A\setminus E$ to itself. It must therefore fix that subset's unique $◃$-least element, contradicting $\pi (a)=b$. Hence $A$ is linearly ordered by the empty-supported dense order but is not well-orderable. Since F2 implies well-orderability of every set, AC fails.