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.