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 = 0s -> ( ph <-> ps ) )
	n0sind.2	|- ( x = y -> ( ph <-> ch ) )
	n0sind.3	|- ( x = ( y +s 1s ) -> ( ph <-> th ) )
	n0sind.4	|- ( x = A -> ( ph <-> ta ) )
	n0sind.5	|- ps
	n0sind.6	|- ( y e. NN0_s -> ( ch -> th ) )
Assertion	n0sind	|- ( A e. NN0_s -> ta )

Proof

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