Theorem n0sind

Description: Principle of Mathematical Induction (inference schema). Compare nnind and finds . (Contributed by Scott Fenton, 17-Mar-2025)

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

Proof

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