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→φ↔ψ
nnind.2 ⊢x=y→φ↔χ
nnind.3 ⊢x=y+1→φ↔θ
nnind.4 ⊢x=A→φ↔τ
nnind.5 ⊢ψ
nnind.6 ⊢y∈ℕ→χ→θ
Assertion nnind ⊢A∈ℕ→τ

Proof

Step Hyp Ref Expression
1 nnind.1 ⊢x=1→φ↔ψ
2 nnind.2 ⊢x=y→φ↔χ
3 nnind.3 ⊢x=y+1→φ↔θ
4 nnind.4 ⊢x=A→φ↔τ
5 nnind.5 ⊢ψ
6 nnind.6 ⊢y∈ℕ→χ→θ
7 1nn ⊢1∈ℕ
8 1 elrab ⊢1∈x∈ℕ|φ↔1∈ℕ∧ψ
9 7 5 8 mpbir2an ⊢1∈x∈ℕ|φ
10 elrabi ⊢y∈x∈ℕ|φ→y∈ℕ
11 peano2nn ⊢y∈ℕ→y+1∈ℕ
12 11 a1d ⊢y∈ℕ→y∈ℕ→y+1∈ℕ
13 12 6 anim12d ⊢y∈ℕ→y∈ℕ∧χ→y+1∈ℕ∧θ
14 2 elrab ⊢y∈x∈ℕ|φ↔y∈ℕ∧χ
15 3 elrab ⊢y+1∈x∈ℕ|φ↔y+1∈ℕ∧θ
16 13 14 15 3imtr4g ⊢y∈ℕ→y∈x∈ℕ|φ→y+1∈x∈ℕ|φ
17 10 16 mpcom ⊢y∈x∈ℕ|φ→y+1∈x∈ℕ|φ
18 17 rgen ⊢∀y∈x∈ℕ|φy+1∈x∈ℕ|φ
19 peano5nni ⊢1∈x∈ℕ|φ∧∀y∈x∈ℕ|φy+1∈x∈ℕ|φ→ℕ⊆x∈ℕ|φ
20 9 18 19 mp2an ⊢ℕ⊆x∈ℕ|φ
21 20 sseli ⊢A∈ℕ→A∈x∈ℕ|φ
22 4 elrab ⊢A∈x∈ℕ|φ↔A∈ℕ∧τ
23 21 22 sylib ⊢A∈ℕ→A∈ℕ∧τ
24 23 simprd ⊢A∈ℕ→τ