Recursion and induction in Baire theorem I am studying the book by Brézis on functional analysis and I just read Baire theorem below:

I understood the idea of the proof. My problem is formalizing it. I was trying to deduce the existence of the sequences $(x_n)$ and $(r_n)$ and its properties using recursion, induction and choice. The theorems I have are

Thm. 1 (Recursion): Let $A$ be a set, $a \in A \ $ and $ \ f: A \to A \ $ be a function. Then there exists an unique sequence $ \ b = (b_n) : \mathbb{N} \to A \ $ such that $ \ b_0 = a \ $ and $ \ b_{n+1} = f(b_n) $, $\forall n \in \mathbb{N}$.
Thm. 2 (Induction): Let $ \ K \subset \mathbb{N} \ $ be such that $ \ 0 \in K \ $ and, $ \forall n \in \mathbb{N}$, if $ \ n \in K$, then $ \ n+1 \in K$. Then $ \ K= \mathbb{N}$.

Together with this version of the axiom of choice:

Axiom (of choice): Let $F$ be a set such that $ \ F \neq \varnothing \ $ and $ \ \varnothing \notin F$. Then there exists a choice function $ \ h : F \to \cup F$, ie, $h(P) \in P$, $\forall P \in F$.

I've tried to deduce the existence of a sequence of nonempty sets $ \ (F_n) \in \big[ \wp(X \times \mathbb{R}) \big]^{\mathbb{N}} \ $ using recursion and to extract a sequence $ \ (x_n , r_n) \in F_n \ $, $\forall n \in \mathbb{N}$, using choice. But I was not able to came with a good recursion base function $ \ f : \wp(X \times \mathbb{R}) \to \wp(X \times \mathbb{R})$.
I need hints to find this function or to try another approach. Any help is appreciated. Thanks in advance.
 A: I’d use the axiom of dependent choice ($\mathsf{DC}$), a weaker consequence of the axiom of choice. Let
$$\mathscr{X}=\{\langle x,r,n\rangle\in X\times\Bbb R^+\times\Bbb N:\operatorname{cl}B(x,r)\subseteq O_n\}\;,$$
and define a relation $R$ on $\mathscr{X}$ by setting $\langle x,r,n\rangle\mathrel{R}\langle y,s,m\rangle$ iff


*

*$m=n+1$,  

*$\operatorname{cl}B(y,s)\subseteq B(x,r)\cap O_m$, and  

*$s<\frac{r}2$.


$\mathsf{DC}$ then gives you a sequence $\big\langle\langle x_k,r_k,k\rangle:k\in\Bbb N\big\rangle$ such that
$$\langle x_k,r_k,k\rangle\mathrel{R}\langle x_{k+1},r_{k+1},k+1\rangle$$
for each $k\in\Bbb N$.
Added: You can adapt this idea to your tools. Let $I=X\times\Bbb R^+\times\Bbb N$, and for each $\langle x,r,n\rangle\in I$ let
$$A(x,r,n)=\left\{\langle y,s,n+1\rangle\in I:s<\frac{r}2\text{ and }\operatorname{cl}B(y,s)\subseteq B(x,r)\cap O_n\right\}\;.$$
Let $\mathscr{A}=\{A(x,r,n):\langle x,r,n\rangle\in I\}$, and let $h$ be a choice function for $\mathscr{A}$. Use $h$ to define a function $f:I\to I$ to which you can apply the recursion theorem to get a suitable sequence $\big\langle\langle x_n,r_n,n\rangle:n\in\Bbb N\big\rangle$.
A: What you really need is the Principle of Dependent Choices, meaning that you have to proceed with a countable number of arbitrary choices such that the (n+1)-th choice depends on the n-th choice, say. In fact, the Baire Theorem for Complete Metric Spaces was shown to be equivalent to the Principle of Dependent Choices by Blair in 1979. 
Blair, Charles E. (1977), "The Baire category theorem implies the principle of dependent choices.", Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., v. 25 n. 10, pp. 933–934.
