Theorem nat_recursion

The Dedekind recursion theorem. It states that there exists exactly one mapping f: ℕ → X that satisfies the recurrence
  f (n + 1) = φ n (f n)
with initial value f 0 = x₀. Here, x₀ may be any element and φ n x any term. It is the corresponding recursion theorem to the induction principle for natural numbers.

Proof sketch
The existence of f is shown in nat_rec_existence, its uniqueness in nat_rec_uniqueness.

Proof
let rec f ↔ app f 0 = x0 ∧
  (∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)).
01. 1 ⊢ set X, hypo.
02. 2 ⊢ x0 ∈ X, hypo.
03. 3 ⊢ ∀n. n ∈ ℕ → ∀x. x ∈ X → φ n x ∈ X, hypo.
04. 1, 2, 3 ⊢ ∃f. set f ∧ (map f ℕ X ∧ rec f), nat_rec_existence 1 2 3.
05. 5 ⊢ map f ℕ X ∧ rec f, hypo.
06. 6 ⊢ map g ℕ X ∧ rec g, hypo.
07. 5 ⊢ map f ℕ X, conj_eliml 5.
08. 6 ⊢ map g ℕ X, conj_eliml 6.
09. 5 ⊢ rec f, conj_elimr 5.
10. 6 ⊢ rec g, conj_elimr 6.
11. 5, 6 ⊢ ∀n. n ∈ ℕ → app f n = app g n,
  nat_rec_uniqueness 9 10, φ n x = φ n x.
12. 5, 6 ⊢ f = g, map_extensionality 7 8 11.
13. ⊢ map f ℕ X ∧ rec f → map g ℕ X ∧ rec g → f = g,
  subj_intro_ii 12.
14. ⊢ ∀g. map f ℕ X ∧ rec f → map g ℕ X ∧ rec g → f = g,
  uq_intro 13.
15. ⊢ ∀f. ∀g. map f ℕ X ∧ rec f → map g ℕ X ∧ rec g → f = g,
  uq_intro 14.
16. 1, 2, 3 ⊢ ∃g. set g ∧ ∀f. g = f ↔ map f ℕ X ∧ rec f, ex_uniq_set_intro 4 15.
nat_recursion. ⊢ set X → x0 ∈ X →
  (∀n. n ∈ ℕ → ∀x. x ∈ X → φ n x ∈ X) → ∃g. set g ∧ ∀f. g = f ↔ map f ℕ X ∧
  (app f 0 = x0 ∧ ∀n. n ∈ ℕ → app f (n + 1) = φ n (app f n)),
  subj_intro_iii 16.

Dependencies
The given proof depends on 18 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, power, radd_assoc, radd_closed, radd_inv, radd_neutr, real_is_set, rle_compat_add, rle_trans, rneg_closed, subset, union.