Theorem peano2nn 5935

Description: Peano postulate: a successor of a natural number is a natural number.

Assertion

Ref	Expression
peano2nn	|- (A e. NN -> (A + 1) e. NN)

Proof of Theorem peano2nn

Step	Hyp	Ref	Expression
1		opreq1 3968	. . 3 |- (z = A -> (z + 1) = (A + 1))
2	1	eleq1d 1540	. 2 |- (z = A -> ((z + 1) e. NN <-> (A + 1) e. NN))
3		opreq1 3968	. . . . . . . . 9 |- (y = z -> (y + 1) = (z + 1))
4	3	eleq1d 1540	. . . . . . . 8 |- (y = z -> ((y + 1) e. x <-> (z + 1) e. x))
5	4	rcla4cv 1874	. . . . . . 7 |- (A.y e. x (y + 1) e. x -> (z e. x -> (z + 1) e. x))
6	5	adantl 388	. . . . . 6 |- ((1 e. x /\ A.y e. x (y + 1) e. x) -> (z e. x -> (z + 1) e. x))
7	6	a2i 9	. . . . 5 |- (((1 e. x /\ A.y e. x (y + 1) e. x) -> z e. x) -> ((1 e. x /\ A.y e. x (y + 1) e. x) -> (z + 1) e. x))
8	7	19.20i 992	. . . 4 |- (A.x((1 e. x /\ A.y e. x (y + 1) e. x) -> z e. x) -> A.x((1 e. x /\ A.y e. x (y + 1) e. x) -> (z + 1) e. x))
9		visset 1813	. . . . 5 |- z e. V
10	9	elintab 2544	. . . 4 |- (z e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)} <-> A.x((1 e. x /\ A.y e. x (y + 1) e. x) -> z e. x))
11		oprex 3983	. . . . 5 |- (z + 1) e. V
12	11	elintab 2544	. . . 4 |- ((z + 1) e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)} <-> A.x((1 e. x /\ A.y e. x (y + 1) e. x) -> (z + 1) e. x))
13	8, 10, 12	3imtr4 219	. . 3 |- (z e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)} -> (z + 1) e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
14		df-n 5925	. . . 4 |- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	14	eleq2i 1538	. . 3 |- (z e. NN <-> z e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
16	14	eleq2i 1538	. . 3 |- ((z + 1) e. NN <-> (z + 1) e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
17	13, 15, 16	3imtr4 219	. 2 |- (z e. NN -> (z + 1) e. NN)
18	2, 17	vtoclga 1852	1 |- (A e. NN -> (A + 1) e. NN)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  {cab 1463  A.wral 1645  |^|cint 2533  (class class class)co 3963  1c1 5235   + caddc 5237  NNcn 5296

This theorem is referenced by:  dfnn2 5936  nnind 5937  nnaddclt 5940  nnleltp1t 5954  nnltp1let 5955  nnsub 5956  nnunb 6070  elnn0nn 6171  nneo 6197  monoord 6294  seq1lem2 6310  seq1suclem 6316  seq1res 6327  ser1recl 6331  ser1p1 6336  ser1mono 6337  ser1add2 6338  ser1add 6339  expp1t 6574  seq1bnd 6910  ser1absdiflem 6929  facp1t 6936  bccl2t 6971  binomlem5 7070  caucvglem5 7161  ser1const 7171  ser1cmp 7174  ser1cmp2 7177  cvgcmp2lem 7180  fnsmnt 7226  cvgratlem1ALT 7247  cvgratlem3ALT 7249  cvgratlem1 7250  cvgratlem3 7252  cvgratlem4 7253  efcltlem1 7304  ef1tllem 7381  eirrlem1 7389  eirrlem3 7391  eirrlem5 7393  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  acdcALT 7496  infpnlem1 7506  infpnlem2 7507  ruclem8 7517  ruclem15 7524  ruclem18 7527  ruclem19 7528  ruclem20 7529  ruclem21 7530  ruclem24 7533  ruclem26 7535  ruclem27 7536  ruclem28 7537  ruclem30 7539  ruclem31 7540  ruclem35 7544  fsumcnlem 7989  bcthlem2 8000  bcthlem17 8015  bcthlem18 8016

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-int 2534  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198  df-opr 3965  df-n 5925

Copyright terms: Public domain