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	⊢ ( 𝑥 = 0s → ( 𝜑 ↔ 𝜓 ) )
	n0sind.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
	n0sind.3	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝜑 ↔ 𝜃 ) )
	n0sind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	n0sind.5	⊢ 𝜓
	n0sind.6	⊢ ( 𝑦 ∈ ℕ0s → ( 𝜒 → 𝜃 ) )
Assertion	n0sind	⊢ ( 𝐴 ∈ ℕ0s → 𝜏 )

Proof

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