Solution (source code)

= Solution

Work in <ZF> with the <law of excluded middle>, without the <axiom of choice>. The paper's terminology is an <infinite Dedekind-finite set>. The useful common principle is <countable union of explicitly ordered finite lists without choice>: given an actual <sequence> of finite lists, enumerate their entries by list number and position using a <Cantor pairing function>. If the union of entries is infinite, repeatedly take the entry with the least code not already selected. This produces an injection from $\mathbb N$ without choosing any enumerations of unordered <sets>.

Consequently, if a family of objects has an explicitly ordered finite list of labels for each object, and only finitely many objects can be made from any given finite pool of labels, then a countably infinite list of distinct objects forces a countably infinite subset of the label <set>. For a Dedekind-finite label <set> this is impossible. If the label <set> embeds into the object family as well, infinitude is preserved. Thus
$$
\boxed{\text{explicit ordered finite supports + finite pools of objects preserve infinite Dedekind-finiteness.}}
$$
The distinction between ordered lists supplied by the data and arbitrary finite subsets is essential: a blanket countable-union theorem for unordered <finite sets> would introduce a choice principle.