LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Dependent choice implies countable choice

Statement

In ZF, the Axiom of Dependent Choice implies the Axiom of Countable Choice: every at most countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Choice function, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

Facts & Assumptions

[A1]

$D C$ : for every nonempty set $X$ , every relation $R \subseteq X \times X$ entire on $X$ and every $a \in X$ there is a function $x : N \to X$ with $x_{0} = a$ and $x_{n} R x_{n + 1}$ for every $n$ (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The natural numbers $N$ (von Neumann), A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

[A2]

${A C}_{ω}$ : for every family $(E_{n})_{n \in N}$ of nonempty sets there is a function $f$ with domain $N$ and $f (n) \in E_{n}$ for all $n$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). A choice function on the set $E : = {E_{n} : n \in N}$ instead has domain $E$ and selects an element of each of its members (Choice function).

[A3]

For sets $A$ and $B$ the collection of functions $A \to B$ is a set (For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$ , The power set $P (x) = {z : z \subseteq x}$ , The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ , The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ ); unions and intersections of indexed families are available ( $⋃_{i \in I} A_{i} : = ⋃ {A_{i} : i \in I}$ , and $⋂_{i \in I} A_{i} : = ⋂ {A_{i} : i \in I}$ for $I \neq \emptyset$ ), induction on $N$ is available (The principle of mathematical induction, The natural numbers $N$ (von Neumann)), and every nonempty subset of $N$ has a least element (The well-ordering principle); a natural number is the set of its predecessors, so $⋃_{n \in N} n = N$ .

Proof

technique · direct

Given: $D C$ and a family $(E_{n})_{n \in N}$ of nonempty sets.

1.1

Let $H$ be the set of all functions $s$ with $dom s \in N$ and $s (j) \in E_{j}$ for every $j < dom s$ : this is a set by [A3] applied inside $⋃_{n \in N} E_{n}$ , and the empty function lies in $H$ , so $H \neq \emptyset$ .

2.1

Define $R \subseteq H \times H$ by $s R t$ if and only if $dom t = dom s + 1$ and $t (j) = s (j)$ for every $j < dom s$ . Then $R$ is entire on $H$ : given $s \in H$ , the set $E_{dom s}$ is nonempty, and for any $x \in E_{dom s}$ the function $t : = s \cup {(dom s, x)}$ lies in $H$ with $s R t$ .

step 1.1A1

3.1

By [A1] applied to $H$ , $R$ and the empty function there is a sequence $(s_{n})_{n \in N}$ in $H$ with $s_{0} = \emptyset$ and $s_{n} R s_{n + 1}$ for every $n$ .

step 1.1step 2.1A1

4.1

For every $n$ one has $dom s_{n} = n$ , by induction on $n$ from [A3]: $dom s_{0} = dom \emptyset = 0$ , and $dom s_{n + 1} = dom s_{n} + 1 = n + 1$ .

step 3.1A3

4.2

The union $f : = ⋃_{n \in N} s_{n}$ is a function: if $(j, y)$ and $(j, y^{'})$ lie in $f$ , they lie in $s_{m}$ and $s_{m^{'}}$ for some $m, m^{'}$ , and with $m \leq m^{'}$ the relation gives $s_{m} \subseteq s_{m^{'}}$ , so $y = y^{'}$ .

step 3.1A3

5.1

Its domain is $N$ : $dom f = ⋃_{n} dom s_{n} = ⋃_{n} n = N$ by [step 4.1] and [A3].

step 4.1A3

5.2

For every $n \in N$ one has $f (n) = s_{n + 1} (n) \in E_{n}$ : the point $n$ lies in $dom s_{n + 1}$ by [step 4.1] and $s_{n + 1} \in H$ with $dom s_{n + 1} = n + 1 > n$ .

step 4.1

6.1

Put $E : = {E_{n} : n \in N}$ . For each $E \in E$ , the set ${n : E_{n} = E}$ is a nonempty subset of $N$ , so let $n (E)$ be its least element and define $c (E) : = f (n (E))$ . Then $c$ has domain $E$ and $c (E) \in E_{n (E)} = E$ , so $c$ is a choice function on the set of members even when the indexed family has repetitions.

step 5.2A2A3

7.1

Hence $f$ is a function with domain $N$ and $f (n) \in E_{n}$ for every $n$ , which is exactly the indexed conclusion of [A2], while $c$ is the corresponding choice function on the set of member sets. Since the family was arbitrary, $D C$ implies ${A C}_{ω}$ .

step 4.2step 5.1step 5.2step 6.1A2∎

Depends on

Used by

Dependency tree · two levels

40 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

H. Herrlich, Axiom of Choice, Lecture Notes in Mathematics 1876 — the finite-history proof that DC implies AC_omega (standard reference, not scraped)