Theorem peano2nn 6080

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 4026	. . 3 |- (z = A -> (z + 1) = (A + 1))
2	1	eleq1d 1583	. 2 |- (z = A -> ((z + 1) e. NN <-> (A + 1) e. NN))
3		opreq1 4026	. . . . . . . . 9 |- (y = z -> (y + 1) = (z + 1))
4	3	eleq1d 1583	. . . . . . . 8 |- (y = z -> ((y + 1) e. x <-> (z + 1) e. x))
5	4	rcla4cv 1920	. . . . . . 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 1028	. . . 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 1859	. . . . 5 |- z e. V
10	9	elintab 2611	. . . 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 4041	. . . . 5 |- (z + 1) e. V
12	11	elintab 2611	. . . 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	3imtr4i 217	. . 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 6070	. . . 4 |- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	14	eleq2i 1581	. . 3 |- (z e. NN <-> z e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
16	14	eleq2i 1581	. . 3 |- ((z + 1) e. NN <-> (z + 1) e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
17	13, 15, 16	3imtr4i 217	. 2 |- (z e. NN -> (z + 1) e. NN)
18	2, 17	vtoclga 1898	1 |- (A e. NN -> (A + 1) e. NN)

Syntax hints:   -> wi 3   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  {cab 1505  A.wral 1691  |^|cint 2600  (class class class)co 4021  1c1 5389   + caddc 5391  NNcn 5450

This theorem is referenced by:  dfnn2 6081  nnind 6082  nnaddcl 6085  nnleltp1 6100  nnltp1le 6101  nnsubi 6102  nnunb 6238  elnn0nn 6339  nneoi 6368  monoord 6482  seq1lem2 6675  seq1suclem 6681  seq1res 6692  ser1recli 6696  ser1p1i 6701  ser1monoi 6702  ser1add2i 6703  ser1addi 6704  expp1 6769  seq1bndi 7113  ser1absdiflem 7132  facp1 7139  bccl2 7174  binomlem5 7273  caucvglem5 7364  ser1consti 7374  ser1cmpi 7377  ser1cmp2i 7380  cvgcmp2lem 7383  arisumi 7430  cvgratlem1ALT 7452  cvgratlem3ALT 7454  cvgratlem1 7455  cvgratlem3 7457  cvgratlem4 7458  efcltlem1 7509  ef1tllem 7586  eirrlem1 7594  eirrlem3 7596  eirrlem5 7598  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  acdcALT 7708  infpnlem1 7718  infpnlem2 7719  ruclem8 7729  ruclem15 7736  ruclem18 7739  ruclem19 7740  ruclem20 7741  ruclem21 7742  ruclem24 7745  ruclem26 7747  ruclem27 7748  ruclem28 7749  ruclem30 7751  ruclem31 7752  ruclem35 7756  fsumcnlem 8200  bcthlem2 8211  bcthlem17 8226  bcthlem18 8227  gxnn0suc 8320  sdc 11877  seqpo 11878  incsequz 11879  incsequz2 11880  mettrifi 11912  geomcau 11914  heiborlem31 12041  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  bfplem3 12056  bfplem5 12058  bfplem6 12059  bfplem8 12061

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-int 2601  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023  df-n 6070

Copyright terms: Public domain