Theorem onat_induction

Proof
01. 1 ⊢ P ∅, hypo.
02. 2 ⊢ ∀n. n ∈ onat → P n → P (succ n), hypo.
03. ⊢ {n | n ∈ onat ∧ P n} ⊆ onat, sep_is_subclass.
04. 1 ⊢ ∅ ∈ onat ∧ P ∅, conj_intro zero_in_onat 1.
05. 1 ⊢ ∅ ∈ {n | n ∈ onat ∧ P n}, comp_intro empty_set_is_set 4.
06. 6 ⊢ n ∈ {n | n ∈ onat ∧ P n}, hypo.
07. 6 ⊢ n ∈ onat ∧ P n, comp_elim 6.
08. 6 ⊢ n ∈ onat, conj_eliml 7.
09. 6 ⊢ P n, conj_elimr 7.
10. 2, 6 ⊢ P n → P (succ n), uq_bounded_elim 2 8.
11. 2, 6 ⊢ P (succ n), subj_elim 10 09.
12. 6 ⊢ succ n ∈ onat, succ_in_onat 8.
13. 6 ⊢ set (succ n), set_intro 12.
14. 2, 6 ⊢ succ n ∈ onat ∧ P (succ n), conj_intro 12 11.
15. 2, 6 ⊢ succ n ∈ {n | n ∈ onat ∧ P n},
  comp_intro 13 14, P n ↔ n ∈ onat ∧ P n.
16. 2 ⊢ n ∈ {n | n ∈ onat ∧ P n} →
  succ n ∈ {n | n ∈ onat ∧ P n}, subj_intro 15.
17. 2 ⊢ ∀n. n ∈ {n | n ∈ onat ∧ P n} →
  succ n ∈ {n | n ∈ onat ∧ P n}, uq_intro 16.
18. 1, 2 ⊢ {n | n ∈ onat ∧ P n} = onat, onat_induction_sets 3 5 17.
19. 19 ⊢ n ∈ onat, hypo.
20. 1, 2, 19 ⊢ n ∈ {n | n ∈ onat ∧ P n}, eq_subst_rev 18 19.
21. 1, 2, 19 ⊢ n ∈ onat ∧ P n, comp_elim 20.
22. 1, 2, 19 ⊢ P n, conj_elimr 21.
23. 1, 2 ⊢ n ∈ onat → P n, subj_intro 22.
24. 1, 2 ⊢ ∀n. n ∈ onat → P n, uq_intro 23.
onat_induction. ⊢ P ∅ → (∀n. n ∈ onat → P n → P (succ n)) →
  (∀n. n ∈ onat → P n), subj_intro_ii 24.

Dependencies
The given proof depends on eight axioms:
comp, eq_refl, eq_subst, ext, infinity, pairing, subset, union.