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	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜓 ) )
	nnind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	nnind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
	nnind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	nnind.5	⊢ 𝜓
	nnind.6	⊢ ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) )
Assertion	nnind	⊢ ( 𝐴 ∈ ℕ → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		nnind.1	⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜓 ) )
2		nnind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		nnind.3	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) )
4		nnind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		nnind.5	⊢ 𝜓
6		nnind.6	⊢ ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) )
7		1nn	⊢ 1 ∈ ℕ
8	1	elrab	⊢ ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 1 ∈ ℕ ∧ 𝜓 ) )
9	7 5 8	mpbir2an	⊢ 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
10		elrabi	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑦 ∈ ℕ )
11		peano2nn	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
12	11	a1d	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ ) )
13	12 6	anim12d	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 ∈ ℕ ∧ 𝜒 ) → ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) ) )
14	2	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ ∧ 𝜒 ) )
15	3	elrab	⊢ ( ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) )
16	13 14 15	3imtr4g	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) )
17	10 16	mpcom	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } )
18	17	rgen	⊢ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 }
19		peano5nni	⊢ ( ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) → ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 } )
20	9 18 19	mp2an	⊢ ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 }
21	20	sseli	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } )
22	4	elrab	⊢ ( 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝐴 ∈ ℕ ∧ 𝜏 ) )
23	21 22	sylib	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℕ ∧ 𝜏 ) )
24	23	simprd	⊢ ( 𝐴 ∈ ℕ → 𝜏 )