This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )