Theorem nn0sinds

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

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

Proof

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