Proof
let inductive A ↔ ∅ ∈ A ∧ (∀n. n ∈ A → n ∪ {n} ∈ A).
01. 1 ⊢ A ∈ {A | inductive A}, hypo.
02. 1 ⊢ ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A, comp_elim 1.
03. 1 ⊢ ∅ ∈ A, conj_eliml 2.
04. ⊢ A ∈ {A | inductive A} → ∅ ∈ A, subj_intro 3.
05. ⊢ ∀A. A ∈ {A | inductive A} → ∅ ∈ A, uq_intro 4.
06. ⊢ ∅ ∈ ⋂{A | inductive A}, Intersection_intro empty_set_is_set 5.
zero_in_onat. ⊢ ∅ ∈ onat, eq_subst_rev onat_eq 6, P x ↔ ∅ ∈ x.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, infinity.