The Mostowski collapse of a finite chain computes its order type

The five numerals are as stated and each of $0,1,2,3,4$ is an ordinal: $0=\mathrm{\varnothing }$ is an ordinal, and $1=0^{+}$, $2=1^{+}$, $3=2^{+}$, $4=3^{+}$ are ordinals by the successor clause, while $4=\{0,1,2,3\}$ by the von Neumann convention.

The order $d\prec a\prec b\prec c$ makes $W$ a well-order: it is total and trichotomous by the given chain, and a nonempty subset of $W$ has a least element, namely the first of its elements in the listing $d,a,b,c$. The initial segments are $W_{<d}=\mathrm{\varnothing }$, $W_{<a}=\{d\}$, $W_{<b}=\{d,a\}$ and $W_{<c}=\{d,a,b\}$, read off from the chain.

The collapse takes the values $F(d)=\mathrm{\varnothing }=0$, $F(a)=\{0\}=1$, $F(b)=\{0,1\}=2$, $F(c)=\{0,1,2\}=3$: by [F3] the map $F$ satisfies $F(x)=\{F(y):y\prec x\}$ for every $x\in W$, and step 1.2 lists the predecessors, so $F(d)=\{\}=\mathrm{\varnothing }$, $F(a)=\{F(d)\}=\{0\}$, $F(b)=\{F(d),F(a)\}=\{0,1\}$, $F(c)=\{F(d),F(a),F(b)\}=\{0,1,2\}$; the identifications with $0,1,2,3$ are [F5].

The image of $F$ is $\{0,1,2,3\}$: the four values are distinct, since $0=\mathrm{\varnothing }$ has no members, $1=\{0\}$ has exactly the member $0$, $2=\{0,1\}$ has exactly the members $0,1$, and $3=\{0,1,2\}$ has the additional member $2$ by [F5]. Moreover $x\prec y$ if and only if $F(x)\in F(y)$ for all $x,y\in W$: the six strict comparisons of the chain read $0\in 1$, $0\in 2$, $0\in 3$, $1\in 2$, $1\in 3$, $2\in 3$, each true by [F5], while the six reversed non-comparisons read $1\mathrm{\notin }0$, $2\mathrm{\notin }0$, $3\mathrm{\notin }0$, $2\mathrm{\notin }1$, $3\mathrm{\notin }1$, $3\mathrm{\notin }2$, each true because $0=\mathrm{\varnothing }$ has no members and $1=\{0\}$, $2=\{0,1\}$.

Hence $F$ is an order isomorphism of $W$ onto the ordinal $4=\{0,1,2,3\}$: it is a bijection onto $4$ by step 3.1, and it preserves and reflects the order by step 3.1; since $4$ is an ordinal by step 1.1, the uniqueness clause of [F3] identifies it with the order type of $W$, so $\mathrm{o}\mathrm{t}(W)=4$.

Uniqueness: if $F^{\mathrm{\prime }}$ is any function on $W$ with $F^{\mathrm{\prime }}(x)=\{F^{\mathrm{\prime }}(y):y\prec x\}$ for all $x\in W$, then reading the chain in order and using the predecessor lists of step 1.2 gives $F^{\mathrm{\prime }}(d)=\mathrm{\varnothing }=F(d)$, $F^{\mathrm{\prime }}(a)=\{F^{\mathrm{\prime }}(d)\}=\{0\}=F(a)$, $F^{\mathrm{\prime }}(b)=\{F^{\mathrm{\prime }}(d),F^{\mathrm{\prime }}(a)\}=F(b)$ and $F^{\mathrm{\prime }}(c)=\{F^{\mathrm{\prime }}(d),F^{\mathrm{\prime }}(a),F^{\mathrm{\prime }}(b)\}=F(c)$; so $F^{\mathrm{\prime }}=F$. This is the uniqueness of [F3] verified directly on the finite chain. The order type of $W$ is $4$ and no object is selected anywhere; in particular no choice principle is used.