Theorem nnsind

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

	Ref	Expression
Hypotheses	nnsind.1	⊢ ( 𝑥 = 1s → ( 𝜑 ↔ 𝜓 ) )
	nnsind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	nnsind.3	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝜑 ↔ 𝜃 ) )
	nnsind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	nnsind.5	⊢ 𝜓
	nnsind.6	⊢ ( 𝑦 ∈ ℕs → ( 𝜒 → 𝜃 ) )
Assertion	nnsind	⊢ ( 𝐴 ∈ ℕs → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		nnsind.1	⊢ ( 𝑥 = 1s → ( 𝜑 ↔ 𝜓 ) )
2		nnsind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3		nnsind.3	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝜑 ↔ 𝜃 ) )
4		nnsind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		nnsind.5	⊢ 𝜓
6		nnsind.6	⊢ ( 𝑦 ∈ ℕs → ( 𝜒 → 𝜃 ) )
7		tru	⊢ ⊤
8		dfnns2	⊢ ℕs = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 +s 1s ) ) , 1s ) “ ω )
9	8	a1i	⊢ ( ⊤ → ℕs = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 +s 1s ) ) , 1s ) “ ω ) )
10		1no	⊢ 1s ∈ No
11	10	a1i	⊢ ( ⊤ → 1s ∈ No )
12	5	a1i	⊢ ( ⊤ → 𝜓 )
13	6	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℕs ) → ( 𝜒 → 𝜃 ) )
14	9 11 1 2 3 4 12 13	noseqinds	⊢ ( ( ⊤ ∧ 𝐴 ∈ ℕs ) → 𝜏 )
15	7 14	mpan	⊢ ( 𝐴 ∈ ℕs → 𝜏 )