Bottom-Up proof of Recursion Theorem

Question

I tried to use bottom-up approach to prove the recursive function theorem in set theory(ZFC). But I'm not sure if there's any errors.

Recursive function theorem means for every nonempty set $S$, function $f : S → S$ and $s_0 ∈ S$, there exists a function $g : ℕ → S$ such that $$g(0)=s_0$$ $$g(n+1)=f(g(n))\ \text{,for all}\ n ∈ ℕ$$

My proof:

Let $\varphi (n, h) :=$

$(0,s_0)∈h\ ∧$

$\left[∀(k,s)∈h.\ k∈ℕ∧k\le n\right]\ ∧$

$\left[ ∀ℕ\ni k\le n.∃! s.(n,s) ∈ h \right]\ ∧$

$\left[ ∀(k,s)∈h.\ k<n→(k+1,f(s))∈h \right]$

*edit: $g(s)$ -> $f(s)$

*edit: [$∀k\le n∃!s∈S.(n,s)∈h$] -> [$∀ℕ\ni k\le n∃!s.(k,s)∈h$]

$h_{n+1}(k+1)=f(h_{n+1}(k))$ for all $k$ in $\{0,...,n\}$

Then by induction, it can be proved that for every $n∈ℕ$, $∃!h$ such that $\varphi(n,h)$.**

Use axiom of replacement define set $G= \left\{ h|n∈ℕ,\ \varphi (n,h) \right\} $

$$g = \cup G$$

Then use induction to prove that $ ∀n,m∈ℕ.\ ∀h_n,h_m.\ n\le m ∧\varphi (n,h_n) ∧ \varphi (m,h_m) \ → h_n(n)=h_m(n)$ ***

In other words, ${h_m}\restriction_{\le n}(x)=h_n(x)$ for all $m \ge n$

So $g$ is well defined.

※I added in the proof of **, but it's very long. I still need to make it shorter.

Proof of **:

1. n=0

   • $\varphi (0,\{ (0,s_0) \})$ is true

     1. $(0,s_0) \in \{ (0,s_0) \}$

     2. for all $(k, s)$ in $\{ (0,s_0) \}$, $(k, s)=(0,s_0)$

        so $k \in ℕ$ and $k \le 0$

     3. $\{(0,s_0)\}$ is a well-defined function, with domain $\{0\}$

     4. there's no $k \in ℕ$ s.t. $k < 0$

   • if $\varphi (0,h)$ is true, then $h = \{ (0,s_0) \}$

     Assume $\varphi (0,h)$ is true

     Then $(0,s_0)\in h$

     Also for all $(k, s) \in h$, $k∈ℕ$ and $k\le 0$

     $\Rightarrow\ k=0$

     By $\left[ ∀k\le n.∃! s∈S.(n,s) ∈ h \right]$, $s$ is unique

     $\Rightarrow\ s=s_0$

     $\Rightarrow$ For all $(k, s) \in h$, $(k,s)=(0,s_0)$

     $\Rightarrow\ h = \{(0,s_0)\}$

2. if ** is true for $n$, then ** is also true for $n+1$

   Suppose $\varphi (n,h_n)$ is true

   Let $h_{n+1} = h_n \cup \{(\ n+1, f[h_n[n]]\ )\}$, then

   • $\varphi (n+1,h_{n+1})$ is true

     1. $h_n \subset h_{n+1}$ and $(0,s_0) \in h_n$

        $\Rightarrow (0,s_0) \in h_{n+1}$

     For all $(k,s)$ in h_{n+1}

     2. $k \in ℕ$ and $k \le n+1$. (This is very obvious)

     3. s is unique:

        • Case $k \le n$:

          $s$ is unique in $h_n$, since $\varphi (n,h_n)$ is true

          And $h_{n+1}\restriction_{\le n}=h_n$

          so $s$ is also unique in $h_{n+1}$

        • Case $k = n+1$:

          since $n+1 \notin \text{Domain}(h_n)$

          and $h_{n+1}\setminus h_n =\{(\ n+1, f[h_n[n]]\ )\}$

          also $(k, s)\in h_{n+1}$

          $\Rightarrow s = f(h_n(n))$

     4. $(k+1,f(s))∈h_{n+1}$ or $k >= n+1$

        • Case $k < n$: $(k+1,f(s))∈h$ since $\varphi (n,h_n)$ is true

        • Case $k = n$: $\{(\ n+1, f[h_n[n]]\ )\} \in h_{n+1}$

   • if $\varphi (n+1,h)$ is true, then $h=h_{n+1}$

     Suppose $\varphi (n,h)$ is true and $n \ge 1$

     Observe that $\varphi (n,h\restriction_{\le n})$ is true

     1. $(0,s_0)∈h\restriction_{\le n}$ (This is obvious)

     2. for all $(k,s)∈h\restriction_{\le n}.$

        $k∈ℕ$ because $(k,s)∈h$

        $k\le n$ by the definition of $h\restriction_{\le n}$

     3. if $k∈ℕ$ and $k\le n$, then $∃! s.(k,s) ∈ h\restriction_{\le n}$.

        Since $k∈ℕ ∧ k\le n \Leftrightarrow k \in \text{Domain}(h\restriction_{\le n})$

     4. for all $(k,s)∈h$ with $k<n$

        $(k+1,f(s))∈h$ since $\varphi (n+1,h)$

        $k+1\le n$ since $k<n$

        $\Rightarrow k+1 \in \text{Domain}(h\restriction_{\le n})$

        $\Rightarrow (k+1,f(s))∈h\restriction_{\le n}$

By 1 and 2, ** is true for all $n∈ℕ$