超眼再帰（再び） - イガブロギュ

前回, 超眼再帰についてよく分かっていなかったので, 勉強し直し, 不備を埋めてみました.
何か間違いがありましたら, 教えて頂けると助かります.

超眼再帰
クラス関数 $G:V \rightarrow V$ に対して, あるクラス関数 $F:Ord \rightarrow V$ が一意に存在して, 任意の $\alpha \in Ord$ について
$F(\alpha) = G(F|\alpha)$ .
ここで, $F|X$ は, 関数 $F$ の定義域を $X$ に制限したものを表す.

証明
まず, 次のことを示します.
$G$ と, 任意の順序数 $\alpha$ に対して, 次を満たす関数 $f_{\alpha}:\alpha+1 \rightarrow V$ が一意に存在する.
任意の $\beta \leq \alpha$ に対して, $f_{\alpha}(\beta) = G(f_{\alpha}|\beta)$ …(*)
今, 任意の $\beta < \alpha$ に対して, 上記をを満たす $f_{\beta}$ が一意に存在すると仮定します.
ここで, $x_{\alpha} = \bigcup_{\beta < \alpha}f_{\beta}$ とおくと, $x_{\alpha}$ が関数になることは明らかです.
(これが実際に集合になることは, 置換の公理により確かめられます.)
さらに, $f_{\alpha} = x_{\alpha} \cup \{\alpha,G(x_{\alpha})\}$ とおくと, これが望むものになっていることが分かります.
したがって超眼帰納法(その3)により, (*) が成り立つことが分かります.
よって, $F(\alpha) = f_{\alpha}(\alpha)$ と定義すれば, $f_{\alpha}(\alpha) = G(f_{\alpha}|\alpha) = G(F|\alpha)$ となります.
$F$ の一意性については, 超眼帰納法(その3)より明らかです.

超眼再帰は, 実際には, 次の形で使われることが多いです.

超眼再帰その2
$V$ から $V$ へのクラス関数 $G_1$ , $G_2$ , $G_3$ に対して, あるクラス関数 $F:Ord \rightarrow V$ が一意に存在して, 任意の $\alpha \in Ord$ について
(i) $F(0) = G_1(0)$ .
(ii) 任意の順序数 $\alpha$ について $F(\alpha+1) = G_2(F(\alpha))$ .
(iii) 任意の $0$ でない極限順序数 $\alpha$ について $F(\alpha) = G_3(F|\alpha)$ .

証明は, 上記の証明を後続順序数と極限順序数を分けて書き直すだけで済みます.