Proof
let inductive A ↔ A ⊆ ℝ ∧ 0 ∈ A ∧ (∀n. n ∈ A → n + 1 ∈ A).
01. 1 ⊢ n ∈ ℕ, hypo.
02. 2 ⊢ A ∈ {A | inductive A}, hypo.
03. 2 ⊢ inductive A, comp_elim 2.
04. 2 ⊢ ∀n. n ∈ A → n + 1 ∈ A, conj_elimr 3.
05. 2 ⊢ ℕ ⊆ A, Intersection_is_lower_bound nat_eq 2.
06. 1, 2 ⊢ n ∈ A, incl_elim 5 1.
07. 1, 2 ⊢ n + 1 ∈ A, uq_bounded_elim 4 6.
08. 1 ⊢ A ∈ {A | inductive A} → n + 1 ∈ A, subj_intro 7.
09. 1 ⊢ ∀A. A ∈ {A | inductive A} → n + 1 ∈ A, uq_intro 8.
10. 1 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 1.
11. ⊢ 1 ∈ ℝ, calc.
12. 1 ⊢ n + 1 ∈ ℝ, radd_closed 10 11.
13. 1 ⊢ set (n + 1), set_intro 12.
14. 1 ⊢ n + 1 ∈ ⋂{A | inductive A}, Intersection_intro 13 9.
15. 1 ⊢ n + 1 ∈ ℕ, eq_subst_rev nat_eq 14, P x ↔ n + 1 ∈ x.
succ_in_nat. ⊢ n ∈ ℕ → n + 1 ∈ ℕ, subj_intro 15.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, radd_closed, real_is_set.