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.

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
$\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$.