Theorem peano2nn 5834

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 3907	. . 3 |- (z = A -> (z + 1) = (A + 1))
2	1	eleq1d 1516	. 2 |- (z = A -> ((z + 1) e. NN <-> (A + 1) e. NN))
3		opreq1 3907	. . . . . . . . 9 |- (y = z -> (y + 1) = (z + 1))
4	3	eleq1d 1516	. . . . . . . 8 |- (y = z -> ((y + 1) e. x <-> (z + 1) e. x))
5	4	rcla4cv 1847	. . . . . . 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 968	. . . 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 1788	. . . . 5 |- z e. V
10	9	elintab 2512	. . . 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 3922	. . . . 5 |- (z + 1) e. V
12	11	elintab 2512	. . . 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 5824	. . . 4 |- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	14	eleq2i 1514	. . 3 |- (z e. NN <-> z e. |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)})
16	14	eleq2i 1514	. . 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 1827	1 |- (A e. NN -> (A + 1) e. NN)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 950   = wceq 1099   e. wcel 1105  {cab 1440  A.wral 1621  |^|cint 2501  (class class class)co 3902  1c1 5158   + caddc 5160  NNcn 5219

This theorem is referenced by:  dfnn2 5835  nnind 5836  nnaddclt 5839  nnleltp1t 5852  nnltp1let 5853  nnsub 5854  nnunb 5968  elnn0nn 6069  nneo 6095  monoord 6182  seq1lem2 6198  seq1suclem 6204  seq1res 6215  ser1recl 6219  ser1p1 6224  ser1mono 6225  ser1add2 6226  ser1add 6227  expp1t 6457  seq1bnd 6798  ser1absdiflem 6817  facp1t 6824  bccl2t 6860  binomlem5 6959  caucvglem5 7048  ser1const 7058  ser1cmp 7061  ser1cmp2 7064  cvgcmp2lem 7067  fnsmnt 7112  cvgratlem1ALT 7133  cvgratlem3ALT 7135  cvgratlem1 7136  cvgratlem3 7138  cvgratlem4 7139  efcltlem1 7197  ef1tllem 7274  eirrlem1 7281  eirrlem3 7283  eirrlem5 7285  acdc3lem 7379  acdc2lem2 7382  acdc5lem2 7385  acdclem 7387  acdcALT 7389  infpnlem1 7400  infpnlem2 7401  ruclem8 7411  ruclem15 7418  ruclem18 7421  ruclem19 7422  ruclem20 7423  ruclem21 7424  ruclem24 7427  ruclem26 7429  ruclem27 7430  ruclem28 7431  ruclem30 7433  ruclem31 7434  ruclem35 7438  fsumcnlem 7871  bcthlem2 7882  bcthlem17 7897  bcthlem18 7898

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-int 2502  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161  df-opr 3904  df-n 5824

Copyright terms: Public domain