An explicit well-ordering of the integers: $0\prec 1\prec -1\prec 2\prec -2\prec \cdots$

The relation $\prec$ is irreflexive: $a\prec a$ would require $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }a\mathrm{\mid }$, impossible because the strict order of $\mathbb{Z}$ is irreflexive, or $\mathrm{\mid }a\mathrm{\mid }=\mathrm{\mid }a\mathrm{\mid }$ together with $a\mathrm{\ne }a$, which is false outright.

Trichotomy: let $a\mathrm{\ne }b$. Totality of the order of $\mathbb{Z}$ decides between $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }b\mathrm{\mid }$, $\mathrm{\mid }a\mathrm{\mid }=\mathrm{\mid }b\mathrm{\mid }$ and $\mathrm{\mid }b\mathrm{\mid }<\mathrm{\mid }a\mathrm{\mid }$; the first gives $a\prec b$ and the third gives $b\prec a$. In the middle case $\mathrm{\mid }a\mathrm{\mid }=\mathrm{\mid }b\mathrm{\mid }=x$ we have $x\ge 0$ by [F2]; if $x=0$ then $a=b=0$ by [F2], contradicting $a\mathrm{\ne }b$, so $x>0$, and exactly one of $0<a$, $0<b$ holds: if both held then $a=\mathrm{\mid }a\mathrm{\mid }=x=\mathrm{\mid }b\mathrm{\mid }=b$ by [F1], contradicting $a\mathrm{\ne }b$, while if neither held then $a\le 0$ and $b\le 0$, so $\mathrm{\mid }a\mathrm{\mid }=-a$ and $\mathrm{\mid }b\mathrm{\mid }=-b$ by [F1] and $a=-x=b$, again contradicting $a\mathrm{\ne }b$. Hence in the middle case exactly one of $a\prec b$, $b\prec a$ holds, and $a\mathrm{\ne }b$ throughout.

Transitivity: suppose $a\prec b$ and $b\prec c$, so $\mathrm{\mid }a\mathrm{\mid }\le \mathrm{\mid }b\mathrm{\mid }\le \mathrm{\mid }c\mathrm{\mid }$ and, when the first strict alternative fails at a stage, the corresponding tie clause holds there. If $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }b\mathrm{\mid }$ then $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }c\mathrm{\mid }$ by transitivity of the order of $\mathbb{Z}$, so $a\prec c$. If $\mathrm{\mid }a\mathrm{\mid }=\mathrm{\mid }b\mathrm{\mid }$ with $a\mathrm{\ne }b$ and $0<a$, then $a=\mathrm{\mid }a\mathrm{\mid }>0$ by [F1], so $\mathrm{\mid }b\mathrm{\mid }>0$ and $b\mathrm{\ne }0$; were $0<b$ then $b=\mathrm{\mid }b\mathrm{\mid }=\mathrm{\mid }a\mathrm{\mid }=a$, contradicting $a\mathrm{\ne }b$, so $b\le 0$ by totality and therefore $b<0$; the tie clause of $b\prec c$ fails because it requires $0<b$, so $b\prec c$ must hold through $\mathrm{\mid }b\mathrm{\mid }<\mathrm{\mid }c\mathrm{\mid }$, whence $\mathrm{\mid }a\mathrm{\mid }<\mathrm{\mid }c\mathrm{\mid }$ and $a\prec c$.

Absolute values are nonnegative integers, and they determine the sign: for every integer $a$, $\mathrm{\mid }a\mathrm{\mid }\ge 0$ by [F2], so $\mathrm{\mid }a\mathrm{\mid }=k$ for a unique natural $k$ under the identification of [F6], and $\mathrm{\mid }a\mathrm{\mid }=0$ exactly when $k=0$; if $\mathrm{\mid }a\mathrm{\mid }=m$ with $m\mathrm{\ne }0$, then either $a\ge 0$ and $a=\mathrm{\mid }a\mathrm{\mid }=m$ by [F1], or $a<0$ and $-a=\mathrm{\mid }a\mathrm{\mid }=m$, so $a=-m$ by [F5]. Moreover for $m\mathrm{\ne }0$: $0<m$, because $m\ge 0$ by [F2] while $m\mathrm{\ne }0$, so $0<m$ by [F3]; and adding $-m$ gives $-m<0$ by [F4] and [F5].

The usual order of $\mathbb{Z}$ is not a well-order: $0<1$, because the integer $1=[(1,0)]$ is the image of the natural $1$ under the identification of [F6] and therefore nonnegative, so $0\le 1$; and $1\mathrm{\ne }0$ since the embedding is injective and $1\mathrm{\ne }0$ in $\mathbb{N}$ by [F11]; hence $0<1$ by [F3]. Adding $-1$ to both sides gives $-1<0$ by [F4] and [F5]; adding an arbitrary integer $n$ gives $n+(-1)<n$. So the nonempty set $\mathbb{Z}$ has no $\le$-least element: for every $n\in \mathbb{Z}$ the integer $n+(-1)$ lies strictly below $n$. Hence $(\mathbb{Z},\le )$ is not a well-order in the sense of [F10].

Let $S\subseteq \mathbb{Z}$ be nonempty. The collection $K=\{k\in \mathbb{N}:\mathrm{\mid }s\mathrm{\mid }=k\text{ for some }s\in S\}$, read through the identification of [F6], is a definable subcollection of $\mathbb{N}$, hence a set by [F12], and it is nonempty because every $\mathrm{\mid }s\mathrm{\mid }$ is a nonnegative integer and so equals a unique natural number by step 1.4. By [F8] the set $K$ has a least element $m$, so $m=\mathrm{\mid }{s}_0\mathrm{\mid }$ for some $s_0\in S$, and $m\le \mathrm{\mid }s\mathrm{\mid }$ for every $s\in S$: writing $\mathrm{\mid }s\mathrm{\mid }=k$ with $k\in K$ we have $m\le k$ in $\mathbb{N}$, which is the integer comparison $m\le k$ by [F6].

The initial segments are as claimed. For $a=0$: no $b$ satisfies $b\prec 0$, since the first clause would need $\mathrm{\mid }b\mathrm{\mid }<0$, excluded by $\mathrm{\mid }b\mathrm{\mid }\ge 0$, and the second would need $\mathrm{\mid }b\mathrm{\mid }=0$, which gives $b=0$ and contradicts $b\mathrm{\ne }0$; hence $W_{<0}=\mathrm{\varnothing }$ by [F9]. For $a\mathrm{\ne }0$ write $\mathrm{\mid }a\mathrm{\mid }=p$ with $p\mathrm{\ne }0$ and $a=p$ or $a=-p$ by step 1.4. For any $b$, the first clause $\mathrm{\mid }b\mathrm{\mid }<\mathrm{\mid }a\mathrm{\mid }$ is equivalent to $k<p$, where $\mathrm{\mid }b\mathrm{\mid }=k$ under the identification of [F6]: if $k<p$ then $k<p$ as integers again by [F6], while if $k\ge p$ then $p\le k$ in $\mathbb{N}$ by [F7], which is the integer comparison $p\le k$, contradicting $\mathrm{\mid }b\mathrm{\mid }<\mathrm{\mid }a\mathrm{\mid }=p$. The integers of absolute value $k$ are exactly $k$ and $-k$ by step 1.4, so the first clause contributes $\{0\}\cup \{\pm n:1\le n<p\}$; the tie clause $\mathrm{\mid }b\mathrm{\mid }=\mathrm{\mid }a\mathrm{\mid }$, $b\mathrm{\ne }a$, $0<b$ forces $b=\mathrm{\mid }b\mathrm{\mid }=p$ by [F1], which differs from $a$ exactly when $a=-p$, contributing $\{-a\}$ when $a<0$ and nothing when $a>0$. Hence $W_{<a}=\{0\}\cup \{\pm n:1\le n<p\}\cup \{-a\}$ for $a<0$ and $W_{<a}=\{0\}\cup \{\pm n:1\le n<p\}$ for $a>0$.

Case $m=0$ of step 2.1: some $s_0\in S$ has $\mathrm{\mid }{s}_0\mathrm{\mid }=0$, so $s_0=0$ by [F2], and $0$ is $\prec$-least in $S$: for $s\in S$ we have $\mathrm{\mid }s\mathrm{\mid }\ge 0=\mathrm{\mid }0\mathrm{\mid }$, so either $\mathrm{\mid }s\mathrm{\mid }>\mathrm{\mid }0\mathrm{\mid }$, giving $0\prec s$ by the first clause, or $\mathrm{\mid }s\mathrm{\mid }=0$, giving $s=0$ by [F2].

Case $m\mathrm{\ne }0$ of step 2.1: then $0<m$ and $-m<0$ by step 1.4, and by step 2.1 there is $s_0\in S$ with $\mathrm{\mid }{s}_0\mathrm{\mid }=m$, so $s_0=m$ or $s_0=-m$ by step 1.4. If $m\in S$ put $\mathrm{\ell }=m$; if $m\mathrm{\notin }S$ put $\mathrm{\ell }=-m$, which lies in $S$ because $s_0\in S$ and the alternative $s_0=m$ is excluded. In both cases $\mathrm{\ell }\in S$ and $\mathrm{\mid }\mathrm{\ell }\mathrm{\mid }=m$, and for every $s\in S$ step 2.1 gives $m\le \mathrm{\mid }s\mathrm{\mid }$ in the integer order: if $\mathrm{\mid }s\mathrm{\mid }>\mathrm{\mid }\mathrm{\ell }\mathrm{\mid }$ then $\mathrm{\ell }\prec s$ by the first clause, while if $\mathrm{\mid }s\mathrm{\mid }=\mathrm{\mid }\mathrm{\ell }\mathrm{\mid }$ then $s=m$ or $s=-m$ by step 1.4, and either $s=\mathrm{\ell }$, or $s=-m$ with $\mathrm{\ell }=m$, in which case $\mathrm{\ell }\mathrm{\ne }s$ and $0<\mathrm{\ell }$, so $\mathrm{\ell }\prec s$ by the tie clause. Since $\prec$ is trichotomous by step 1.2, no $s\in S$ satisfies $s\prec \mathrm{\ell }$: $\mathrm{\ell }$ is $\prec$-least in $S$.

Every nonempty $S\subseteq \mathbb{Z}$ has a $\prec$-least element: step 2.1 produces the natural $m$ of least absolute value, and steps 3.1 and 3.2 cover the cases $m=0$ and $m\mathrm{\ne }0$. Together with irreflexivity, transitivity and trichotomy from steps 1.1 to 1.3 this exhibits $\prec$ as the strict presentation of a well-order of $\mathbb{Z}$; the initial segments are those computed in step 2.2; and the usual order of $\mathbb{Z}$ is not a well-order by step 1.5, so the usual order and the explicit well-order of the same set are different. The relation is given by one explicit formula and no object is selected at any stage, so no choice principle is used.