Theorem onat_induction_sets

Proof
01. 1 ⊢ A ⊆ onat, hypo.
02. 2 ⊢ ∅ ∈ A, hypo.
03. 3 ⊢ ∀n. n ∈ A → succ n ∈ A, hypo.
04. 4 ⊢ n ∈ A, hypo.
05. 3, 4 ⊢ succ n ∈ A, uq_bounded_elim 3 4.
06. 3, 4 ⊢ n ∪ {n} ∈ A, eq_subst succ_eq 5, P x ↔ x ∈ A.
07. 3 ⊢ n ∈ A → n ∪ {n} ∈ A, subj_intro 6.
08. 3 ⊢ ∀n. n ∈ A → n ∪ {n} ∈ A, uq_intro 7.
09. 2, 3 ⊢ ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A, conj_intro 2 8.
10. 1 ⊢ set A, subset 1 onat_is_set.
11. 1, 2, 3 ⊢ A ∈ {A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A},
  comp_intro 10 09.
12. 1, 2, 3 ⊢ A ∈ onat_inductive_sets,
  eq_subst_rev onat_inductive_sets_eq 11, P x ↔ A ∈ x.
13. 1, 2, 3 ⊢ onat ⊆ A, Intersection_is_lower_bound onat_eq 12.
14. 1, 2, 3 ⊢ A = onat, incl_antisym 1 13.
onat_induction_sets. ⊢ A ⊆ onat → ∅ ∈ A →
  (∀n. n ∈ A → succ n ∈ A) → A = onat, subj_intro_iii 14.

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