Corollary 6.9 — Systems of distinct representatives

For every type $\iota$ equipped with a finite enumeration, every type $\alpha$, and every family of sets $A_i\subseteq\alpha$ indexed by $i\in\iota$, the following assertions are equivalent: there exists a function $f:\iota\to\alpha$ such that $f(i)\in A_i$ for every $i$ and $f$ is injective, meaning that $f(i)=f(j)$ implies $i=j$ for all indices $i,j$; and, for every finite set $I$ of indices, $|I|\leq\left|\bigcup_{i\in I}A_i\right|$ as an inequality in $\mathbb N\cup\{\infty\}$. On the left of this inequality, the ordinary finite cardinality of $I$ is embedded into the extended natural numbers. On the right, the union has its ordinary finite cardinality if it is finite and has value $\infty$ if it is infinite, regardless of the size of that infinite set; thus an infinite union automatically satisfies the inequality for that particular $I$. The union counts each element of $\alpha$ once even if it belongs to several sets of the family. Only the index type is assumed finite: $\alpha$ and individual sets $A_i$ may be finite, infinite, or empty, and no decidable-equality or nonemptiness assumption is made on either type. Different indices may index equal sets, but their chosen representatives must still be distinct. The existence of $f$ does not assert that it is unique. The condition includes $I=\varnothing$, when it is $0\leq0$. If the index type is empty, both assertions hold, including when $\alpha$ is empty, since the empty function is injective and satisfies all membership requirements. If any indexed set $A_i$ is empty, both assertions are false, with the singleton index set $\{i\}$ violating the inequality; in particular, when $\alpha$ is empty and the index type is nonempty, both assertions are false. Infinite index types are outside the hypotheses.