LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every natural-number-indexed list of nonempty sets has a choice function on its family of values

Statement

Let $n \in N$ and let $F$ be a function with domain $n$ all of whose values are nonempty sets. Then the family of its values, $F = F [n] = {F (i) : i \in n}$ , has a choice function (Choice function).

This is a theorem of ZF: its proof uses no form of the Axiom of Choice (The Axiom of Choice).

What is proved below is exactly the displayed statement, by induction on $n$ . The natural number $n$ serves as the index set in the von Neumann sense, $n = {0, 1, \dots, n - 1}$ (The natural numbers $N$ (von Neumann)), so " $F$ has domain $n$ " says precisely that the members of $F$ are listed as $F (0), \dots, F (n - 1)$ . The listing need not be injective, and $F$ is the set of values, so repetitions are harmless and are not counted.

The displayed statement and its proof use only a natural-number-indexed function. They do not identify an arbitrary finite family with a particular enumeration.

Facts & Assumptions

Given: A natural number $n$ , used as the index set $n = {0, \dots, n - 1}$ , and a function $F$ with domain $n$ such that $F (i) \neq \emptyset$ for every $i \in n$ ; write $F [n] = {F (i) : i \in n}$ for the family of values of $F$ .

[A1]

$P (n)$ denotes the statement: for every function $F$ with domain $n$ all of whose values are nonempty sets, the family $F [n]$ has a choice function.

[L1]

Induction principle: if $P (0)$ holds and $P (n)$ implies $P (n + 1)$ for every $n \in N$ , then $P (n)$ holds for every $n \in N$ , where $n + 1$ denotes the successor $σ (n)$ (The principle of mathematical induction, Addition of natural numbers).

[L2]

A choice function for a family $F$ is a function $g$ with domain $F$ such that $g (S) \in S$ for every $S \in F$ (Choice function).

[L3]

$0 = \emptyset$ and $σ (n) = n \cup {n}$ , so $n \subseteq σ (n)$ (The natural numbers $N$ (von Neumann)). Thus a function $F$ with domain $σ (n)$ restricts to a function with domain $n$ ; moreover, directly from the definition of image, $y \in F [σ (n)]$ iff $y = F (i)$ for some $i \in n$ or $y = F (n)$ , so $F [σ (n)] = F [n] \cup {F (n)}$ .

Proof

technique · induction

1.1

Base case: $0 = \emptyset$ , so the only function with domain $0$ is the empty function, its family of values is $F [0] = \emptyset$ , and the empty function has domain $\emptyset$ and satisfies the defining condition vacuously, so it is a choice function for $F [0]$ ; hence $P (0)$ holds.

baseA1L2L3

1.2

Inductive hypothesis: fix $n \in N$ and assume $P (n)$ , that every function with domain $n$ whose values are all nonempty has a choice function for its family of values.

ihA1

1.3

Let $F$ be an arbitrary function with domain $σ (n) = n \cup {n}$ all of whose values are nonempty sets; write $S = F (n)$ and $G = F [n]$ , the family of values of the restriction $F ↾ n$ , so that $F [σ (n)] = G \cup {S}$ .

givenL3

2.1

The restriction $F ↾ n$ is a function with domain $n$ , and every value of it is a value of $F$ , hence nonempty; so the inductive hypothesis applies to it and supplies a choice function $h$ for $G$ , a function with domain $G$ satisfying $h (T) \in T$ for every $T \in G$ .

step 1.3step 1.2L2L3

2.2

The set $S = F (n)$ is one of the values of $F$ , hence nonempty, so there exists an element of $S$ ; fix one and call it $a$ .

step 1.3choose

3.1

Define $g = (h ↾ (G ∖ {S})) \cup {(S, a)}$ ; its two pieces are functions with the disjoint domains $G ∖ {S}$ and ${S}$ , so $g$ is a function, and its domain is $(G ∖ {S}) \cup {S} = G \cup {S} = F [σ (n)]$ .

step 2.1step 2.2step 1.3construct

4.1

Every $T \in F [σ (n)]$ is either $S$ or a member of $G ∖ {S}$ ; in the first case $g (S) = a \in S$ , and in the second $g (T) = h (T) \in T$ because $h$ is a choice function for $G$ . So $g (T) \in T$ throughout.

step 3.1step 2.1step 2.2

5.1

Hence $g$ is a choice function for $F [σ (n)]$ , and since $F$ was an arbitrary function with domain $σ (n)$ with nonempty values, $P (n)$ implies $P (n + 1)$ .

step 4.1step 3.1step 1.3L2A1

6.1

By the induction principle, $P (n)$ holds for every $n \in N$ : the family of values of any function whose domain is a natural number and whose values are nonempty has a choice function.

step 1.1step 5.1L1discharge-induction∎

Remarks

Later finiteness terminology. A finite set is defined later as one equinumerous with a natural number (Finite, countably infinite, countable, uncountable ↗). That terminology is not used in the proof above, which keeps its exact indexed-family scope.
Where the Axiom of Choice would be needed, and why it is not needed here. Step 2.2 picks one element out of one nonempty set. That is a single existential instantiation, licensed by first-order logic alone. The induction performs one such instantiation per stage, and the stages are indexed by a natural number, so the process terminates. ZF cannot in general turn an arbitrary infinite family of nonempty sets into a simultaneous choice function; that is the gap The Axiom of Choice fills. An infinite family with a distinguished element in each member may still have an explicit choice function in ZF, as Russell's shoes and socks ↗ shows.
Why the family is presented as an indexed one. Stated over "a family of exactly $n$ sets", the successor step would have to assert that deleting one member of a family of $n + 1$ sets leaves exactly $n$ , which is a claim about cardinality and needs a theory of finiteness this page does not have. Indexed by $n$ , the same step is the restriction $F ↾ n$ of a function, which is immediate from $n \subseteq σ (n)$ and costs nothing. Nothing else in the argument changes.
The listing may repeat, and the argument is arranged so that repetition needs no separate treatment: $g$ is built by overwriting rather than by adjoining, so it is a function whether or not $S$ already occurs among $F (0), \dots, F (n - 1)$ . In particular $F$ may have strictly fewer than $n$ members.
The lemma is not a special case of the Axiom of Choice that happens to be provable; it is the precise boundary of what is free. Russell's shoes and socks ↗ makes the boundary concrete, and Finite choice written out: a choice function for three sets ↗ works this induction out on a small family.

Depends on

Used by

…and 40 more results.

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Axiom of choice (Wikipedia) (standard reference, not scraped)
Choice function (Wikipedia) (standard reference, not scraped)