| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. |
| Ref | Expression |
|---|---|
| peano2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano2b 4102 |
. 2
| |
| 2 | 1 | biimpi 224 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: nnacl 5447 nnecl 5449 nnmsucr 5458 1onn 5471 2onn 5472 dif1en 5842 findcard 5843 findcard2 5844 unbnn2 5857 axinf2 5963 dfom3 5972 noinfep 5983 trcl 5988 cardsucnn 6141 dif1card 6143 dif1cardOLD 6144 omsublim 6178 alephfp 6231 domtriomlem 6296 domtriomlemOLD 6298 axdc2lem 6303 axdc3lem 6305 axdc3lem2 6306 axdc3lem4 6308 axdc4lem 6310 axdclem2 6372 om2uzrani 8082 uzrdgsuci 8087 fzennn 8090 cardfzOLD 8092 bnj924 13604 omopthlem1 14501 trpredtr 14582 top2usne 15655 fictblem 16194 omsublimOLD 16220 neibastop2lem4 16346 findcard2OLD 16569 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1592 ax-gen 1593 ax-8 1594 ax-9 1595 ax-10 1596 ax-11 1597 ax-12 1598 ax-13 1599 ax-14 1600 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-10o 1781 ax-16 1854 ax-11o 1864 ax-ext 2123 ax-sep 3606 ax-nul 3613 ax-pow 3649 ax-pr 3687 ax-un 3929 |
| This theorem depends on definitions: df-bi 220 df-or 338 df-an 339 df-3or 1103 df-3an 1104 df-ex 1616 df-sb 1816 df-eu 2041 df-mo 2042 df-clab 2129 df-cleq 2134 df-clel 2137 df-ne 2268 df-ral 2359 df-rex 2360 df-rab 2362 df-v 2540 df-dif 2830 df-un 2832 df-in 2834 df-ss 2836 df-pss 2838 df-nul 3083 df-if 3181 df-pw 3229 df-sn 3242 df-pr 3243 df-tp 3245 df-op 3246 df-uni 3367 df-br 3508 df-opab 3566 df-tr 3580 df-eprel 3744 df-po 3752 df-so 3764 df-fr 3782 df-we 3798 df-ord 3814 df-on 3815 df-lim 3816 df-suc 3817 df-om 4086 |