Proof
let inductive A ↔ A ⊆ ℝ ∧ 0 ∈ A ∧ (∀n. n ∈ A → n + 1 ∈ A).
01. 1 ⊢ A ∈ {A | inductive A}, hypo.
02. 1 ⊢ inductive A, comp_elim 1.
03. 1 ⊢ 0 ∈ A, conj_elimlr 2.
04. ⊢ A ∈ {A | inductive A} → 0 ∈ A, subj_intro 3.
05. ⊢ ∀A. A ∈ {A | inductive A} → 0 ∈ A, uq_intro 4.
06. ⊢ 0 ∈ ℝ, calc.
07. ⊢ set 0, set_intro 6.
08. ⊢ 0 ∈ ⋂{A | inductive A}, Intersection_intro 7 5.
zero_in_nat. ⊢ 0 ∈ ℕ, eq_subst_rev nat_eq 8, P x ↔ 0 ∈ x.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.