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