I have the following homework assignment:
Let $\textbf{V} \models ZFC$ and let $\mathbb{P} = (P, \leq)$ be a forcing partial order in $\textbf{V}$. Define a class function $F: \textbf{V} \to \textbf{V}$ such that using the transfinite recursion theorem there exists a function $G: \Omega \to \textbf{V}$ such that for all $\alpha \in \Omega$: $ G(\alpha) = V_\alpha^{\mathbb{P}}$
What follows is my answer, can you please tell me if I have it right:
(i) For $\alpha = \emptyset $ we want $G(\alpha) = V_\emptyset^\mathbb{P} = 0 =: F(0)$
(ii) For $\alpha = 1$ we want $G(1) = V_1^\mathbb{P} = \mathcal{P}( V_\emptyset^\mathbb{P}\times \mathbb{P}) = \mathcal{P}( \emptyset \times \mathbb{P}) \cong \mathcal{P}(\emptyset) = \{\emptyset\} = 1 =: F(G|_1)$
For $\alpha = 2$ we want $G(2) = V_2^\mathbb{P} = \mathcal{P}(V_1^\mathbb{P} \times \mathbb{P}) = \mathcal{P}(\{\emptyset\} \times \mathbb{P}) =: F(G|_2)$
So for a successor ordinal $\alpha \in \Omega$ we define $F(G|_{\alpha + 1}) := \mathcal{P}(F(G|_\alpha) \times \mathbb{P})$
(iii) For a limit ordinal $\alpha \in \Omega$, we have $V_\alpha^\mathbb{P} = \cup_{\beta \in \alpha} V_\beta^\mathbb{P}$ and so we want to define $G(\alpha) = \cup_{\beta \in \alpha} V_\beta^\mathbb{P} = \cup_{\beta \in \alpha} F(G|_\beta) =: F(G|_\alpha)$
Is this all I need to do? Or do I need to show that $F$ is well-defined or anything else? Many thanks for your help!