For $F \subseteq \Bbb R$, the derived set of $F$, denoted by $F'$, is the set of all limit points of $F$.
Prove that there exists a unique transfinite sequence $\langle F_\alpha \rangle_{\alpha \in \rm{Ord}}$ of subsets of $\Bbb R$ such that
$$\begin{align} F_0 &= F \subseteq \Bbb R\\ F_{\alpha+1} &= (F_{\alpha})' \space \text{ for all } \alpha \in \rm{Ord}\\ F_{\alpha} &= \bigcap_{\xi < \alpha} F_{\xi} \text{ for all limit ordinal } \alpha \end{align}$$
Does my attempt look fine or contain logical flaws/gaps? Any suggestion is greatly appreciated. Thank you for your help!
My attempt:
Let $V$ be the class of all sets. We define a class function $\mathcal G: V \to V$ by $$ \mathcal G(x)=\begin{cases} x' &\text{ if } x \subseteq \Bbb R\\ \bigcap \rm{ran}(x) & \text{ if }x \text{ is a non-empty function}\\\emptyset & \text { otherwise } \end{cases}$$
By Transfinite Recursion Theorem, there exists a unique class function $\mathcal F:\rm{Ord} \to V$ such that
$\mathcal F(0)=F$
$\mathcal F(\alpha+1)=\mathcal G(\mathcal F(\alpha))$ for all $\alpha\in\operatorname{Ord}$
$\mathcal F(\alpha)=\mathcal G(\mathcal F\restriction\alpha)$ for all limit $\alpha\neq 0$
- $\mathcal F(\alpha) \subseteq \Bbb R$ for all $\alpha\in\operatorname{Ord}$
We have $\mathcal F(0)=F \subseteq \Bbb R$.
If $\mathcal F(\alpha) \subseteq \Bbb R$, then $\mathcal G(\mathcal F(\alpha))=(\mathcal F(\alpha))'\subseteq \Bbb R$ by the definition of $\mathcal G$. So $\mathcal F(\alpha+1)=\mathcal G(\mathcal F(\alpha))\subseteq \Bbb R$.
If $\mathcal F(\xi) \subseteq \Bbb R$ for all $\xi < \alpha$ where $\alpha$ is a limit ordinal. It follows from the construction of $\mathcal G$ that $\mathcal F(\alpha)=\mathcal G(\mathcal F\restriction\alpha)=\bigcap \rm{ran}(\mathcal F\restriction\alpha)=\bigcap_{\xi < \alpha} \mathcal F(\xi) \subseteq \Bbb R$. Thus $\mathcal F(\alpha) \subseteq \Bbb R$.
- $\mathcal F(\alpha+1) = (\mathcal F(\alpha))'$ for all $\alpha\in\operatorname{Ord}$
We have $\mathcal F(\alpha+1)=\mathcal G(\mathcal F(\alpha))$. From 1., we have $\mathcal F(\alpha) \subseteq \Bbb R$ for all $\alpha\in\operatorname{Ord}$. Then $\mathcal G(\mathcal F(\alpha)) = (F(\alpha))'$ by the construction of $\mathcal G$. Thus $\mathcal F(\alpha+1) = (\mathcal F(\alpha))'$.
- If $\alpha$ is a limit ordinal, then $\mathcal F(\alpha) = \bigcap_{\xi < \alpha} \mathcal F(\xi)$
Since $\alpha$ is a limit ordinal, $\mathcal F(\alpha)=\mathcal G(\mathcal F\restriction\alpha) =\bigcap \rm{ran}(\mathcal F\restriction\alpha)$ by the construction of $\mathcal G$. We have $\bigcap \rm{ran}(\mathcal F\restriction\alpha)=\bigcap_{\xi < \alpha} \mathcal F(\xi)$. Thus $\mathcal F(\alpha) = \bigcap_{\xi < \alpha} \mathcal F(\xi)$.
We define sequence $\langle F_\alpha \rangle_{\alpha \in \rm{Ord}}$ by $F_\alpha=\mathcal F(\alpha)$. It follows that
$$\begin{align} F_0 &= F\\ F_{\alpha+1} &= (F_{\alpha})' \space \text{ for all } \alpha \in \rm{Ord}\\ F_{\alpha} &= \bigcap_{\xi < \alpha} F_{\xi} \text{ for all limit ordinal } \alpha \end{align}$$