Axiom of Dependent Choice

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $\omega$ be as in The Class Omega of Natural Numbers with Zero §omega, let $\mathbb{N}$ and $1$ be as in The Set of Natural Numbers and the Number One §naturals and The Set of Natural Numbers and the Number One §one, and let $+$ be the addition on $\omega$. Then $1\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 §one, and $m+1\in\mathbb{N}$ for every $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 §closed.

¶ Let $b$ be a set, let $R$ be a relation on $b$ such that for every $u\in b$ there is $v\in b$ with $(u,v)\in R$, and let $s\in b$. Then there is a map $f:\mathbb{N}\to b$, written as the family $(f_{m})_{m\in\mathbb{N}}$, such that $f_{1}=s$ and $(f_{m},f_{m+1})\in R$ for every $m\in\mathbb{N}$.