Theorem onat_induction_sets

Proof
let inductive A ↔ ∅ ∈ A ∧ (∀n. n ∈ A → n ∪ {n} ∈ A).
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 ⊢ inductive A, conj_intro 2 8.
10. 1 ⊢ set A, subset 1 onat_is_set.
11. 1, 2, 3 ⊢ A ∈ {A | inductive A},
  comp_intro 10 09.
12. 1, 2, 3 ⊢ onat ⊆ A, Intersection_is_lower_bound onat_eq 11.
13. 1, 2, 3 ⊢ A = onat, incl_antisym 1 12.
onat_induction_sets. ⊢ A ⊆ onat → ∅ ∈ A →
  (∀n. n ∈ A → succ n ∈ A) → A = onat, subj_intro_iii 13.

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