Theorem nn0sinds

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

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

Proof

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