Proof of Countable Choice Follows from Dependent Choice

Let $b$ and $(A_{m})_{m\in\mathbb{N}}$ be as in the clause countable-choice above. By Indexed Families of Sets and Their Union, Intersection and Product §family, the family is a function $A$ with domain $\mathbb{N}$, and for $n\in\mathbb{N}$, $A_{n}$ is its value at $n$, a set. By The Set of Natural Numbers and the Number One §naturals, $\mathbb{N}=\omega\setminus\{0\}$ is a set, and by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations every element of $\mathbb{N}$ lies in $\omega$; let $1$ be as in The Set of Natural Numbers and the Number One §one. By Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one, $1\in\mathbb{N}$, and by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §closed, $n+1\in\mathbb{N}$ for every $n\in\mathbb{N}$, where $+$ is the addition on $\omega$. Membership in a class formed by class abstraction is unfolded by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, without further mention below. Contrary to the convention of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §notation, the upper-case letters $X$ and $R$ below denote sets.

The set of pairs. Let

$$X=\{q:\exists n\,\exists y\,(n\in\mathbb{N}\wedge y\in b\wedge y\in A_{n}\wedge q=(n,y))\},$$

formed by class abstraction with the parameters $\mathbb{N}$, $b$ and $A$. Its formula quantifies over set variables only; the ordered pair and the value $A_{n}$ are defined set symbols, the latter used properly, as the conjunct $n\in\mathbb{N}$ ensures $n\in\operatorname{dom}A$. So the formula is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, for all sets $n$ and $y$,

$$(n,y)\in X\quad\text{if and only if}\quad n\in\mathbb{N},\ y\in b\ \text{and}\ y\in A_{n}.\qquad(1)$$

Every element of $X$ is a pair $(n,y)$ with $n\in\mathbb{N}$ and $y\in b$, hence lies in $\mathbb{N}\times b$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership; so $X\subseteq\mathbb{N}\times b$ by Subclasses and Subsets §subclass. As $\mathbb{N}\times b$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, $X$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.

The relation. Let

$$R=\{r:\exists n\,\exists y\,\exists y'\,(n\in\mathbb{N}\wedge(n,y)\in X\wedge(n+1,y')\in X\wedge r=((n,y),(n+1,y')))\},$$

formed by class abstraction with the parameters $\mathbb{N}$ and $X$. Its formula quantifies over set variables only; the ordered pair and $n+1$ are defined set symbols, the latter by Addition on Omega §addition and used properly, as the conjunct $n\in\mathbb{N}$ gives $n\in\omega$, and $1\in\omega$. So it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, for all sets $u$ and $v$,

$$(u,v)\in R\quad\text{iff}\quad\text{there are sets }n,y,y'\text{ with }n\in\mathbb{N},\ u=(n,y)\in X\text{ and }v=(n+1,y')\in X.\qquad(2)$$

Every element of $R$ is an ordered pair of two elements of $X$, so $R$ is a relation by Relations, Domain, Range, Inverse and Composition §relation, and $R\subseteq X\times X$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and Subclasses and Subsets §subclass; hence $R$ is a relation on $X$ by Relations, Domain, Range, Inverse and Composition §on. As $X\times X$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, $R$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.

Totality. Let $u\in X$. Then $u=(n,y)$ for sets $n,y$ with $n\in\mathbb{N}$, $y\in b$ and $y\in A_{n}$. Since $n+1\in\mathbb{N}$, the set $A_{n+1}$ has an element $y'$ by hypothesis, and $y'\in b$ because $A_{n+1}\subseteq b$, by Subclasses and Subsets §subclass. By (1), $(n+1,y')\in X$, and by (2), $(u,(n+1,y'))\in R$.

Start. Since $1\in\mathbb{N}$, the set $A_{1}$ has an element by hypothesis; fix one, $y_{1}$. Then $y_{1}\in b$ as $A_{1}\subseteq b$, so $s=(1,y_{1})\in X$ by (1).

Dependent choice. By Axiom of Dependent Choice §dependent-choice, applied to the set $X$ in place of $b$, the relation $R$ on $X$ and $s\in X$, there is a map $f:\mathbb{N}\to X$, written $(f_{m})_{m\in\mathbb{N}}$, with $f_{1}=s$ and $(f_{m},f_{m+1})\in R$ for every $m\in\mathbb{N}$. By Functions, Values of a Function, and Functions from One Class to Another §map, $\operatorname{dom}f=\mathbb{N}$ and $\operatorname{ran}f\subseteq X$.

Indices. Let

$$P=\{m\in\mathbb{N}:\exists y\,(f_{m}=(m,y))\},$$

formed by restricted class abstraction with the parameters $\mathbb{N}$ and $f$. Its formula quantifies over the set variable $y$ only; the ordered pair and the value $f_{m}$ are defined set symbols, the latter used properly, as the left conjunct $m\in\mathbb{N}$ ensures $m\in\operatorname{dom}f$. So it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires, and $P\subseteq\mathbb{N}$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Subclasses and Subsets §subclass. First, $f_{1}=(1,y_{1})$, so $1\in P$. Next let $m\in P$, so $f_{m}=(m,y)$ for some set $y$. As $(f_{m},f_{m+1})\in R$, (2) gives sets $n,y'',y'$ with $f_{m}=(n,y'')$ and $f_{m+1}=(n+1,y')$. From $(m,y)=(n,y'')$, The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic gives $m=n$, so $f_{m+1}=(m+1,y')$. Since $m\in\omega$, $m+1=S(m)$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one, where $S(m)$ is the successor of $m$; and $S(m)\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §successors. Thus $f_{S(m)}=(S(m),y')$, and $S(m)\in P$. By The Principle of Induction for the Natural Numbers Starting at One §induction, $P=\mathbb{N}$.

The choice map. Let

$$x=\{q:\exists m\,\exists y\,(m\in\mathbb{N}\wedge f_{m}=(m,y)\wedge q=(m,y))\},$$

formed by class abstraction with the parameters $\mathbb{N}$ and $f$; as for $P$, its formula is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, for all sets $m$ and $y$,

$$(m,y)\in x\quad\text{if and only if}\quad m\in\mathbb{N}\ \text{and}\ f_{m}=(m,y).\qquad(3)$$

Function. Every element of $x$ is an ordered pair, so $x$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. If $(m,y)\in x$ and $(m,y')\in x$, then $(m,y)=f_{m}=(m,y')$ by (3), so $y=y'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic. Hence $x$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function.

Domain. By Relations, Domain, Range, Inverse and Composition §domain and (3), every $m\in\operatorname{dom}x$ lies in $\mathbb{N}$. Conversely, for $m\in\mathbb{N}=P$ there is a set $y$ with $f_{m}=(m,y)$, so $(m,y)\in x$ by (3) and $m\in\operatorname{dom}x$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}x=\mathbb{N}$.

Values. Let $m\in\mathbb{N}$ and let $y=x_{m}$ be the value of $x$ at $m$, so $(m,y)\in x$ by Functions, Values of a Function, and Functions from One Class to Another §value, and $f_{m}=(m,y)$ by (3). Since $(m,f_{m})\in f$, $f_{m}\in\operatorname{ran}f$ by Relations, Domain, Range, Inverse and Composition §range, so $(m,y)=f_{m}\in X$. By (1), $y\in b$ and $y\in A_{m}$; that is, $x_{m}\in A_{m}$ and $x_{m}\in b$.

Range. Let $v\in\operatorname{ran}x$. By Relations, Domain, Range, Inverse and Composition §range there is a set $m$ with $(m,v)\in x$; then $m\in\operatorname{dom}x=\mathbb{N}$, and $v=x_{m}$ by Functions, Values of a Function, and Functions from One Class to Another §value, so $v\in b$ by the values just computed. Hence $\operatorname{ran}x\subseteq b$ by Subclasses and Subsets §subclass, and $x:\mathbb{N}\to b$ by Functions, Values of a Function, and Functions from One Class to Another §map. Every element of $x$ is a pair $(m,x_{m})$ with $m\in\mathbb{N}$ and $x_{m}\in b$, so $x\subseteq\mathbb{N}\times b$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and $x$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set and Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass. Written as the family $(x_{m})_{m\in\mathbb{N}}$ as in Indexed Families of Sets and Their Union, Intersection and Product §family, it satisfies $x_{m}\in A_{m}$ for every $m\in\mathbb{N}$.