Theorem nnsind

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

	Ref	Expression
Hypotheses	nnsind.1	|- ( x = 1s -> ( ph <-> ps ) )
	nnsind.2	|- ( x = y -> ( ph <-> ch ) )
	nnsind.3	|- ( x = ( y +s 1s ) -> ( ph <-> th ) )
	nnsind.4	|- ( x = A -> ( ph <-> ta ) )
	nnsind.5	|- ps
	nnsind.6	|- ( y e. NN_s -> ( ch -> th ) )
Assertion	nnsind	|- ( A e. NN_s -> ta )

Proof

Step	Hyp	Ref	Expression
1		nnsind.1	|- ( x = 1s -> ( ph <-> ps ) )
2		nnsind.2	|- ( x = y -> ( ph <-> ch ) )
3		nnsind.3	|- ( x = ( y +s 1s ) -> ( ph <-> th ) )
4		nnsind.4	|- ( x = A -> ( ph <-> ta ) )
5		nnsind.5	|- ps
6		nnsind.6	|- ( y e. NN_s -> ( ch -> th ) )
7		tru	|- T.
8		dfnns2	|- NN_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 1s ) " _om )
9	8	a1i	|- ( T. -> NN_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 1s ) " _om ) )
10		1sno	|- 1s e. No
11	10	a1i	|- ( T. -> 1s e. No )
12	5	a1i	|- ( T. -> ps )
13	6	adantl	|- ( ( T. /\ y e. NN_s ) -> ( ch -> th ) )
14	9 11 1 2 3 4 12 13	noseqinds	|- ( ( T. /\ A e. NN_s ) -> ta )
15	7 14	mpan	|- ( A e. NN_s -> ta )