Theorem succ_in_onat

Proof
01. 1 ⊢ n ∈ onat, hypo.
02. 2 ⊢ A ∈ onat_inductive_sets, hypo.
03. 2 ⊢ A ∈ {A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A},
  eq_subst onat_inductive_sets_eq 2.
04. 2 ⊢ ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A, comp_elim 3.
05. 2 ⊢ ∀n. n ∈ A → n ∪ {n} ∈ A, conj_elimr 4.
06. 2 ⊢ onat ⊆ A, Intersection_is_lower_bound onat_eq 2.
07. 1, 2 ⊢ n ∈ A, incl_elim 6 1.
08. 1, 2 ⊢ n ∪ {n} ∈ A, uq_bounded_elim 5 7.
09. 1, 2 ⊢ succ n ∈ A, eq_subst_rev succ_eq 8, P x ↔ x ∈ A.
10. 1 ⊢ A ∈ onat_inductive_sets → succ n ∈ A, subj_intro 9.
11. 1 ⊢ ∀A. A ∈ onat_inductive_sets → succ n ∈ A, uq_intro 10.
12. 1 ⊢ set n, set_intro 1.
13. 1 ⊢ set (succ n), succ_is_set 12.
14. 1 ⊢ succ n ∈ ⋂onat_inductive_sets, Intersection_intro 13 11.
15. 1 ⊢ succ n ∈ onat, eq_subst_rev onat_eq 14, P x ↔ succ n ∈ x.
succ_in_onat. ⊢ n ∈ onat → succ n ∈ onat, subj_intro 15.

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