# Metamath Proof Explorer

## Theorem nnind

Description: Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl for an example of its use. See nn0ind for induction on nonnegative integers and uzind , uzind4 for induction on an arbitrary upper set of integers. See indstr for strong induction. See also nnindALT . This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 16-Jun-2013)

Ref Expression
Hypotheses nnind.1 ${⊢}{x}=1\to \left({\phi }↔{\psi }\right)$
nnind.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
nnind.3 ${⊢}{x}={y}+1\to \left({\phi }↔{\theta }\right)$
nnind.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
nnind.5 ${⊢}{\psi }$
nnind.6 ${⊢}{y}\in ℕ\to \left({\chi }\to {\theta }\right)$
Assertion nnind ${⊢}{A}\in ℕ\to {\tau }$

### Proof

Step Hyp Ref Expression
1 nnind.1 ${⊢}{x}=1\to \left({\phi }↔{\psi }\right)$
2 nnind.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
3 nnind.3 ${⊢}{x}={y}+1\to \left({\phi }↔{\theta }\right)$
4 nnind.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
5 nnind.5 ${⊢}{\psi }$
6 nnind.6 ${⊢}{y}\in ℕ\to \left({\chi }\to {\theta }\right)$
7 1nn ${⊢}1\in ℕ$
8 1 elrab ${⊢}1\in \left\{{x}\in ℕ|{\phi }\right\}↔\left(1\in ℕ\wedge {\psi }\right)$
9 7 5 8 mpbir2an ${⊢}1\in \left\{{x}\in ℕ|{\phi }\right\}$
10 elrabi ${⊢}{y}\in \left\{{x}\in ℕ|{\phi }\right\}\to {y}\in ℕ$
11 peano2nn ${⊢}{y}\in ℕ\to {y}+1\in ℕ$
12 11 a1d ${⊢}{y}\in ℕ\to \left({y}\in ℕ\to {y}+1\in ℕ\right)$
13 12 6 anim12d ${⊢}{y}\in ℕ\to \left(\left({y}\in ℕ\wedge {\chi }\right)\to \left({y}+1\in ℕ\wedge {\theta }\right)\right)$
14 2 elrab ${⊢}{y}\in \left\{{x}\in ℕ|{\phi }\right\}↔\left({y}\in ℕ\wedge {\chi }\right)$
15 3 elrab ${⊢}{y}+1\in \left\{{x}\in ℕ|{\phi }\right\}↔\left({y}+1\in ℕ\wedge {\theta }\right)$
16 13 14 15 3imtr4g ${⊢}{y}\in ℕ\to \left({y}\in \left\{{x}\in ℕ|{\phi }\right\}\to {y}+1\in \left\{{x}\in ℕ|{\phi }\right\}\right)$
17 10 16 mpcom ${⊢}{y}\in \left\{{x}\in ℕ|{\phi }\right\}\to {y}+1\in \left\{{x}\in ℕ|{\phi }\right\}$
18 17 rgen ${⊢}\forall {y}\in \left\{{x}\in ℕ|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{y}+1\in \left\{{x}\in ℕ|{\phi }\right\}$
19 peano5nni ${⊢}\left(1\in \left\{{x}\in ℕ|{\phi }\right\}\wedge \forall {y}\in \left\{{x}\in ℕ|{\phi }\right\}\phantom{\rule{.4em}{0ex}}{y}+1\in \left\{{x}\in ℕ|{\phi }\right\}\right)\to ℕ\subseteq \left\{{x}\in ℕ|{\phi }\right\}$
20 9 18 19 mp2an ${⊢}ℕ\subseteq \left\{{x}\in ℕ|{\phi }\right\}$
21 20 sseli ${⊢}{A}\in ℕ\to {A}\in \left\{{x}\in ℕ|{\phi }\right\}$
22 4 elrab ${⊢}{A}\in \left\{{x}\in ℕ|{\phi }\right\}↔\left({A}\in ℕ\wedge {\tau }\right)$
23 21 22 sylib ${⊢}{A}\in ℕ\to \left({A}\in ℕ\wedge {\tau }\right)$
24 23 simprd ${⊢}{A}\in ℕ\to {\tau }$