Theorem zero_in_onat

Proof
01. 1 ⊢ A ∈ onat_inductive_sets, hypo.
02. 1 ⊢ A ∈ {A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A},
  eq_subst onat_inductive_sets_eq 1.
03. 1 ⊢ ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A, comp_elim 2.
04. 1 ⊢ ∅ ∈ A, conj_eliml 3.
05. ⊢ A ∈ onat_inductive_sets → ∅ ∈ A, subj_intro 4.
06. ⊢ ∀A. A ∈ onat_inductive_sets → ∅ ∈ A, uq_intro 5.
07. ⊢ ∅ ∈ ⋂onat_inductive_sets, Intersection_intro empty_set_is_set 6.
zero_in_onat. ⊢ ∅ ∈ onat, eq_subst_rev onat_eq 7, P x ↔ ∅ ∈ x.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, infinity.