Theorem nnind

Description: Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl for an example of its use. See nn0ind for induction on nonnegative integers and uzind , uzind4 for induction on an arbitrary upper set of integers. See indstr for strong induction. See also nnindALT . This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 16-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		nnind.1	|- ( x = 1 -> ( ph <-> ps ) )
2		nnind.2	|- ( x = y -> ( ph <-> ch ) )
3		nnind.3	|- ( x = ( y + 1 ) -> ( ph <-> th ) )
4		nnind.4	|- ( x = A -> ( ph <-> ta ) )
5		nnind.5	|- ps
6		nnind.6	|- ( y e. NN -> ( ch -> th ) )
7		1nn	|- 1 e. NN
8	1	elrab	|- ( 1 e. { x e. NN | ph } <-> ( 1 e. NN /\ ps ) )
9	7 5 8	mpbir2an	|- 1 e. { x e. NN | ph }
10		elrabi	|- ( y e. { x e. NN | ph } -> y e. NN )
11		peano2nn	|- ( y e. NN -> ( y + 1 ) e. NN )
12	11	a1d	|- ( y e. NN -> ( y e. NN -> ( y + 1 ) e. NN ) )
13	12 6	anim12d	|- ( y e. NN -> ( ( y e. NN /\ ch ) -> ( ( y + 1 ) e. NN /\ th ) ) )
14	2	elrab	|- ( y e. { x e. NN | ph } <-> ( y e. NN /\ ch ) )
15	3	elrab	|- ( ( y + 1 ) e. { x e. NN | ph } <-> ( ( y + 1 ) e. NN /\ th ) )
16	13 14 15	3imtr4g	|- ( y e. NN -> ( y e. { x e. NN | ph } -> ( y + 1 ) e. { x e. NN | ph } ) )
17	10 16	mpcom	|- ( y e. { x e. NN | ph } -> ( y + 1 ) e. { x e. NN | ph } )
18	17	rgen	|- A. y e. { x e. NN | ph } ( y + 1 ) e. { x e. NN | ph }
19		peano5nni	|- ( ( 1 e. { x e. NN | ph } /\ A. y e. { x e. NN | ph } ( y + 1 ) e. { x e. NN | ph } ) -> NN C_ { x e. NN | ph } )
20	9 18 19	mp2an	|- NN C_ { x e. NN | ph }
21	20	sseli	|- ( A e. NN -> A e. { x e. NN | ph } )
22	4	elrab	|- ( A e. { x e. NN | ph } <-> ( A e. NN /\ ta ) )
23	21 22	sylib	|- ( A e. NN -> ( A e. NN /\ ta ) )
24	23	simprd	|- ( A e. NN -> ta )