Theorem nnind 6080

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 hypothesis. See nnaddcl 6083 for an example of its use. See nn0ind 6381 for induction on nonnegative integers and uzind 6374, uzind4 6575 for induction on an arbitrary set of upper integers. See indstr 6586 for strong induction.

Hypotheses

Ref	Expression
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

Ref	Expression
nnind	|- (A e. NN -> ta)

Distinct variable groups:   x,y   x,A   ps,x   ch,x   th,x   ta,x   ph,y

Proof of Theorem nnind

Step	Hyp	Ref	Expression
1		nnind.1	. . . . . . 7 |- (x = 1 -> (ph <-> ps))
2	1	elrab 1950	. . . . . 6 |- (1 e. {x e. NN | ph} <-> (1 e. NN /\ ps))
3		1nn 6077	. . . . . 6 |- 1 e. NN
4		nnind.5	. . . . . 6 |- ps
5	2, 3, 4	mpbir2an 734	. . . . 5 |- 1 e. {x e. NN | ph}
6		ssrab2 2182	. . . . . . . 8 |- {x e. NN | ph} (_ NN
7	6	sseli 2116	. . . . . . 7 |- (y e. {x e. NN | ph} -> y e. NN)
8		peano2nn 6078	. . . . . . . . . 10 |- (y e. NN -> (y + 1) e. NN)
9	8	a1d 12	. . . . . . . . 9 |- (y e. NN -> (y e. NN -> (y + 1) e. NN))
10		nnind.6	. . . . . . . . 9 |- (y e. NN -> (ch -> th))
11	9, 10	anim12d 560	. . . . . . . 8 |- (y e. NN -> ((y e. NN /\ ch) -> ((y + 1) e. NN /\ th)))
12		nnind.2	. . . . . . . . 9 |- (x = y -> (ph <-> ch))
13	12	elrab 1950	. . . . . . . 8 |- (y e. {x e. NN | ph} <-> (y e. NN /\ ch))
14		nnind.3	. . . . . . . . 9 |- (x = (y + 1) -> (ph <-> th))
15	14	elrab 1950	. . . . . . . 8 |- ((y + 1) e. {x e. NN | ph} <-> ((y + 1) e. NN /\ th))
16	11, 13, 15	3imtr4g 555	. . . . . . 7 |- (y e. NN -> (y e. {x e. NN | ph} -> (y + 1) e. {x e. NN | ph}))
17	7, 16	mpcom 49	. . . . . 6 |- (y e. {x e. NN | ph} -> (y + 1) e. {x e. NN | ph})
18	17	rgen 1743	. . . . 5 |- A.y e. {x e. NN | ph} (y + 1) e. {x e. NN | ph}
19		nnex 6076	. . . . . . 7 |- NN e. V
20	19	rabex 2798	. . . . . 6 |- {x e. NN | ph} e. V
21	20	peano5nni 6069	. . . . 5 |- ((1 e. {x e. NN | ph} /\ A.y e. {x e. NN | ph} (y + 1) e. {x e. NN | ph}) -> NN (_ {x e. NN | ph})
22	5, 18, 21	mp2an 700	. . . 4 |- NN (_ {x e. NN | ph}
23	22	sseli 2116	. . 3 |- (A e. NN -> A e. {x e. NN | ph})
24		nnind.4	. . . 4 |- (x = A -> (ph <-> ta))
25	24	elrab 1950	. . 3 |- (A e. {x e. NN | ph} <-> (A e. NN /\ ta))
26	23, 25	sylib 196	. 2 |- (A e. NN -> (A e. NN /\ ta))
27	26	pm3.27d 323	1 |- (A e. NN -> ta)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 991   e. wcel 993  A.wral 1690  {crab 1693   (_ wss 2098  (class class class)co 4019  1c1 5387   + caddc 5389  NNcn 5448

This theorem is referenced by:  nnindALT 6081  nn1suc 6082  nnaddcl 6083  nnmulcl 6084  nnge1 6086  nnleltp1 6098  nnsubi 6100  nneoi 6366  uzindOLD 6377  nn0ind-raph 6383  monoord 6480  seq1lem1 6672  seq1rn2 6684  seq1res 6690  ser1recli 6694  ser1add2i 6701  ser1addi 6702  seq1shftid 6719  expcllem 6768  expeq0 6778  expgt1 6784  seq1bndi 7111  ser1absdiflem 7130  bccl2 7172  binomlem6 7272  ser1consti 7372  ser1cmpi 7375  ser1cmp2i 7378  cvgratlem1ALT 7450  cvgratlem1 7453  ruclem25 7744  ruclem32 7751  sdclem2 11769  incsequz 11772  mettrifi 11805  bfplem6 11952

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-nul 2783  ax-pow 2817  ax-pr 2854  ax-un 3088  ax-inf2 4768

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 781  df-3an 782  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-reu 1696  df-rab 1697  df-v 1857  df-sbc 1986  df-csb 2051  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2415  df-pw 2458  df-sn 2469  df-pr 2470  df-tp 2472  df-op 2473  df-uni 2569  df-int 2600  df-iun 2634  df-br 2692  df-opab 2740  df-tr 2754  df-eprel 2909  df-id 2912  df-po 2917  df-so 2928  df-fr 2946  df-we 2961  df-ord 2977  df-on 2978  df-lim 2979  df-suc 2980  df-om 3218  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-fv 3278  df-opr 4021  df-oprab 4022  df-1st 4138  df-2nd 4139  df-rdg 4231  df-1o 4267  df-oadd 4269  df-omul 4270  df-er 4399  df-ec 4401  df-qs 4404  df-ni 5152  df-pli 5153  df-mi 5154  df-lti 5155  df-plpq 5187  df-mpq 5188  df-enq 5189  df-nq 5190  df-plq 5191  df-mq 5192  df-rq 5193  df-ltq 5194  df-1q 5195  df-np 5238  df-1p 5239  df-plp 5240  df-mp 5241  df-ltp 5242  df-plpr 5316  df-mpr 5317  df-enr 5318  df-nr 5319  df-plr 5320  df-mr 5321  df-ltr 5322  df-0r 5323  df-1r 5324  df-m1r 5325  df-c 5392  df-0 5393  df-1 5394  df-i 5395  df-r 5396  df-plus 5397  df-mul 5398  df-sub 5508  df-neg 5510  df-n 6068

Copyright terms: Public domain