Theorem nnsinds

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

	Ref	Expression
Hypotheses	nnsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	nnsinds.2	$$⊢x=N\to \left(\phi \leftrightarrow \chi \right)$$
	nnsinds.3	$$⊢x\in \mathbb{N}\to \left(\forall y\in \left(1\dots x-1\right)\psi \to \phi \right)$$
Assertion	nnsinds	$$⊢N\in \mathbb{N}\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		nnsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		nnsinds.2	$$⊢x=N\to \left(\phi \leftrightarrow \chi \right)$$
3		nnsinds.3	$$⊢x\in \mathbb{N}\to \left(\forall y\in \left(1\dots x-1\right)\psi \to \phi \right)$$
4		elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$
5		elnnuz	$$⊢x\in \mathbb{N}\leftrightarrow x\in {\mathbb{Z}}_{\ge 1}$$
6	5 3	sylbir	$$⊢x\in {\mathbb{Z}}_{\ge 1}\to \left(\forall y\in \left(1\dots x-1\right)\psi \to \phi \right)$$
7	1 2 6	uzsinds	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to \chi$$
8	4 7	sylbi	$$⊢N\in \mathbb{N}\to \chi$$