$\min$ is a choice function on $\mathbb{N}$

Every nonempty subset of $\mathbb{N}$ has a least element (The well-ordering principle), and that least element is unique, so

$\min : \mathcal{P}(\mathbb{N}) \setminus \{\emptyset\} \longrightarrow \mathbb{N}, \qquad \min S = \text{the least element of } S,$

is a well defined function, and $\min S \in S$ by construction. It is therefore a choice function on $\mathbb{N}$ (Choice function), given by a single rule and produced with no appeal to the Axiom of Choice.

What makes the choice free here is the structure of the order (Order on the natural numbers), not the size of the family. The order well-orders $\mathbb{N}$, and a well-order names a canonical element of every nonempty subset; how large the family of nonempty subsets is then does not matter.

• The rule, not the existence, is the point. [L1] gives a least element of each nonempty $S$ separately. Turning a family of separate existence statements into one function is exactly what the Axiom of Choice does in general, and it is exactly what is avoided here: uniqueness of the least element makes "the least element of $S$" a formula in $S$, so the graph of $\min$ is carved out by Separation from $\mathcal{F} \times \mathbb{N}$ with no further axiom.

• Every natural-number-indexed list of nonempty sets has a choice function on its family of values does not apply, and not for the reason usually given. That lemma carries no finiteness hypothesis at all, and it refuses that reading explicitly: it is stated over an indexed family, a natural number $n$ and a function $F$ with domain $n$ all of whose values are nonempty, and it gives a choice function for the family $F[n]$ of the values of $F$. What disqualifies $\mathcal{F} = \mathcal{P}(\mathbb{N}) \setminus \{\emptyset\}$ is that it is not $F[n]$ for any such $F$: sending each member of $F[n]$ to the least index at which $F$ takes it as a value injects $F[n]$ into $n$, the least index existing by [L1], whereas $\mathcal{F}$ already contains the $n + 1$ pairwise distinct singletons $\{0\}, \{1\}, \dots, \{n\}$, and no injection $\sigma(n) \to n$ exists (The pigeonhole principle on $\mathbb{N}$ ↗, which this library proves on a later page). Size is not what is at stake here, structure is, and Russell's shoes and socks is the contrasting case: a family of two element sets, with no listing of this kind and no rule either.

• The same construction works verbatim on any set carrying a well-order, with "least element" read in that order. Whether every arbitrary set carries a well-order is a different question, and answering it affirmatively is again a form of the Axiom of Choice. The library does prove it, but only from that axiom and only on a later page (The well-ordering theorem ↗); nothing in this example uses it, and no item on this page lists it as a dependency.

• Antisymmetry does the whole of the uniqueness work, and it is the only order axiom needed for it. This is the same one-line argument that makes $\sup$ legitimate notation in a poset (Upper bound, least upper bound, and strict upper bound).