Theorem nnsind

Description: Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025)

	Ref	Expression
Hypotheses	nnsind.1	$$⊢x=1_s\to \left(\phi \leftrightarrow \psi \right)$$
	nnsind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	nnsind.3	$$⊢x=y{+}_s{1}_s\to \left(\phi \leftrightarrow \theta \right)$$
	nnsind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	nnsind.5	$$⊢\psi$$
	nnsind.6	$$⊢y\in {\mathbb{N}}_s\to \left(\chi \to \theta \right)$$
Assertion	nnsind	$$⊢A\in {\mathbb{N}}_s\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		nnsind.1	$$⊢x=1_s\to \left(\phi \leftrightarrow \psi \right)$$
2		nnsind.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		nnsind.3	$$⊢x=y{+}_s{1}_s\to \left(\phi \leftrightarrow \theta \right)$$
4		nnsind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		nnsind.5	$$⊢\psi$$
6		nnsind.6	$$⊢y\in {\mathbb{N}}_s\to \left(\chi \to \theta \right)$$
7		tru	$$⊢\top$$
8		dfnns2	$$⊢{\mathbb{N}}_s=\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n{+}_s{1}_s\right),1_s\right)\left[\mathrm{\omega }\right]$$
9	8	a1i	$$⊢\top \to {\mathbb{N}}_s=\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n{+}_s{1}_s\right),1_s\right)\left[\mathrm{\omega }\right]$$
10		1no	$$⊢1_s\in \mathrm{No}$$
11	10	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
12	5	a1i	$$⊢\top \to \psi$$
13	6	adantl	$$⊢\left(\top \wedge y\in {\mathbb{N}}_s\right)\to \left(\chi \to \theta \right)$$
14	9 11 1 2 3 4 12 13	noseqinds	$$⊢\left(\top \wedge A\in {\mathbb{N}}_s\right)\to \tau$$
15	7 14	mpan	$$⊢A\in {\mathbb{N}}_s\to \tau$$