The induction principle for the natural numbers. See wf_induction for a generalization to well-founded relations.
Proof
let M = {n | n ∈ ℕ ∧ P n}.
01. 1 ⊢ P 0, hypo.
02. 2 ⊢ ∀n. n ∈ ℕ → P n → P (n + 1), hypo.
03. ⊢ M ⊆ ℕ, sep_is_subclass.
04. 1 ⊢ 0 ∈ ℕ ∧ P 0, conj_intro zero_in_nat 1.
05. ⊢ set 0, set_intro zero_in_nat.
06. ⊢ set u → Q u → u ∈ {n | Q n}, comp_intro.
07. 1 ⊢ 0 ∈ M, 6 5 4, Q n ↔ n ∈ ℕ ∧ P n.
08. 8 ⊢ n ∈ M, hypo.
09. 8 ⊢ n ∈ ℕ ∧ P n, comp_elim 8.
10. 8 ⊢ n ∈ ℕ, conj_eliml 9.
11. 8 ⊢ P n, conj_elimr 9.
12. 2, 8 ⊢ P n → P (n + 1), uq_bounded_elim 2 10.
13. 2, 8 ⊢ P (n + 1), subj_elim 12 11.
14. 8 ⊢ n + 1 ∈ ℕ, succ_in_nat 10.
15. 8 ⊢ set (n + 1), set_intro 14.
16. 2, 8 ⊢ n + 1 ∈ ℕ ∧ P (n + 1), conj_intro 14 13.
17. 2, 8 ⊢ n + 1 ∈ M, comp_intro 15 16, P n ↔ n ∈ ℕ ∧ P n.
18. 2 ⊢ n ∈ M → n + 1 ∈ M, subj_intro 17.
19. 2 ⊢ ∀n. n ∈ M → n + 1 ∈ M, uq_intro 18.
20. 1, 2 ⊢ M = ℕ, nat_induction_sets 3 7 19.
21. 21 ⊢ n ∈ ℕ, hypo.
22. 1, 2, 21 ⊢ n ∈ M, eq_subst_rev 20 21.
23. 1, 2, 21 ⊢ n ∈ ℕ ∧ P n, comp_elim 22.
24. 1, 2, 21 ⊢ P n, conj_elimr 23.
25. 1, 2 ⊢ n ∈ ℕ → P n, subj_intro 24.
26. 1, 2 ⊢ ∀n. n ∈ ℕ → P n, uq_intro 25.
nat_induction. ⊢ P 0 → (∀n. n ∈ ℕ → P n → P (n + 1)) →
(∀n. n ∈ ℕ → P n), subj_intro_ii 26.
Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, ext, radd_closed, real_is_set, subset.