Theorem nnsinds

Description: Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014)

	Ref	Expression
Hypotheses	nnsinds.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	nnsinds.2	⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) )
	nnsinds.3	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) )
Assertion	nnsinds	⊢ ( 𝑁 ∈ ℕ → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		nnsinds.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		nnsinds.2	⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) )
3		nnsinds.3	⊢ ( 𝑥 ∈ ℕ → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) )
4		elnnuz	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
5		elnnuz	⊢ ( 𝑥 ∈ ℕ ↔ 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
6	5 3	sylbir	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) )
7	1 2 6	uzsinds	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝜒 )
8	4 7	sylbi	⊢ ( 𝑁 ∈ ℕ → 𝜒 )