Metamath Proof Explorer

Theorem nnindf

Description: Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018)

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

Proof

Step Hyp Ref Expression
1 nnindf.x 
 |-  F/ y ph
2 nnindf.1 
 |-  ( x = 1 -> ( ph <-> ps ) )
3 nnindf.2 
 |-  ( x = y -> ( ph <-> ch ) )
4 nnindf.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> th ) )
5 nnindf.4 
 |-  ( x = A -> ( ph <-> ta ) )
6 nnindf.5 
 |-  ps
7 nnindf.6 
 |-  ( y e. NN -> ( ch -> th ) )
8 1nn 
 |-  1 e. NN
9 2 elrab 
 |-  ( 1 e. { x e. NN | ph } <-> ( 1 e. NN /\ ps ) )
10 8 6 9 mpbir2an 
 |-  1 e. { x e. NN | ph }
11 elrabi 
 |-  ( y e. { x e. NN | ph } -> y e. NN )
12 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
13 12 a1d 
 |-  ( y e. NN -> ( y e. NN -> ( y + 1 ) e. NN ) )
14 13 7 anim12d 
 |-  ( y e. NN -> ( ( y e. NN /\ ch ) -> ( ( y + 1 ) e. NN /\ th ) ) )
15 3 elrab 
 |-  ( y e. { x e. NN | ph } <-> ( y e. NN /\ ch ) )
16 4 elrab 
 |-  ( ( y + 1 ) e. { x e. NN | ph } <-> ( ( y + 1 ) e. NN /\ th ) )
17 14 15 16 3imtr4g 
 |-  ( y e. NN -> ( y e. { x e. NN | ph } -> ( y + 1 ) e. { x e. NN | ph } ) )
18 11 17 mpcom 
 |-  ( y e. { x e. NN | ph } -> ( y + 1 ) e. { x e. NN | ph } )
19 18 rgen 
 |-  A. y e. { x e. NN | ph } ( y + 1 ) e. { x e. NN | ph }
20 nfcv 
 |-  F/_ y NN
21 1 20 nfrabw 
 |-  F/_ y { x e. NN | ph }
22 nfcv 
 |-  F/_ w { x e. NN | ph }
23 nfv 
 |-  F/ w ( y + 1 ) e. { x e. NN | ph }
24 21 nfel2 
 |-  F/ y ( w + 1 ) e. { x e. NN | ph }
25 oveq1 
 |-  ( y = w -> ( y + 1 ) = ( w + 1 ) )
26 25 eleq1d 
 |-  ( y = w -> ( ( y + 1 ) e. { x e. NN | ph } <-> ( w + 1 ) e. { x e. NN | ph } ) )
27 21 22 23 24 26 cbvralfw 
 |-  ( A. y e. { x e. NN | ph } ( y + 1 ) e. { x e. NN | ph } <-> A. w e. { x e. NN | ph } ( w + 1 ) e. { x e. NN | ph } )
28 19 27 mpbi 
 |-  A. w e. { x e. NN | ph } ( w + 1 ) e. { x e. NN | ph }
29 peano5nni 
 |-  ( ( 1 e. { x e. NN | ph } /\ A. w e. { x e. NN | ph } ( w + 1 ) e. { x e. NN | ph } ) -> NN C_ { x e. NN | ph } )
30 10 28 29 mp2an 
 |-  NN C_ { x e. NN | ph }
31 30 sseli 
 |-  ( A e. NN -> A e. { x e. NN | ph } )
32 5 elrab 
 |-  ( A e. { x e. NN | ph } <-> ( A e. NN /\ ta ) )
33 31 32 sylib 
 |-  ( A e. NN -> ( A e. NN /\ ta ) )
34 33 simprd 
 |-  ( A e. NN -> ta )