Metamath Proof Explorer


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 ( 𝑁 ∈ ℕ → 𝜒 )