Proof
let inductive A ↔ ∅ ∈ A ∧ (∀n. n ∈ A → n ∪ {n} ∈ A).
01. ⊢ ∃A. set A ∧ inductive A, infinity.
02. 2 ⊢ set A ∧ inductive A, hypo.
03. 2 ⊢ set A, conj_eliml 2.
04. 2 ⊢ inductive A, conj_elimr 2.
05. 2 ⊢ A ∈ {A | inductive A}, comp_intro 3 4.
06. 2 ⊢ onat ⊆ A, Intersection_is_lower_bound onat_eq 5.
07. 2 ⊢ set onat, subset 6 3.
onat_is_set. ⊢ set onat, ex_elim 1 7.
Dependencies
The given proof depends on four axioms:
comp, eq_subst, infinity, subset.