![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > peano2 | Structured version Visualization version Unicode version |
Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
Ref | Expression |
---|---|
peano2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano2b 6713 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 198 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-sbc 3270 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-tr 4501 df-eprel 4748 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-om 6698 |
This theorem is referenced by: onnseq 7068 seqomlem1 7172 seqomlem4 7175 onasuc 7235 onmsuc 7236 onesuc 7237 nnacl 7317 nnecl 7319 nnacom 7323 nnmsucr 7331 1onn 7345 2onn 7346 3onn 7347 4onn 7348 nnneo 7357 nneob 7358 omopthlem1 7361 onomeneq 7767 dif1en 7809 findcard 7815 findcard2 7816 unbnn2 7833 dffi3 7950 wofib 8065 axinf2 8150 dfom3 8157 noinfep 8170 cantnflt 8182 trcl 8217 cardsucnn 8424 dif1card 8446 fseqdom 8462 alephfp 8544 ackbij1lem16 8670 ackbij2lem2 8675 ackbij2lem3 8676 ackbij2 8678 sornom 8712 infpssrlem4 8741 fin23lem26 8760 fin23lem20 8772 fin23lem38 8784 fin23lem39 8785 isf32lem2 8789 isf32lem3 8790 isf34lem7 8814 isf34lem6 8815 fin1a2lem6 8840 fin1a2lem9 8843 fin1a2lem12 8846 domtriomlem 8877 axdc2lem 8883 axdc3lem 8885 axdc3lem2 8886 axdc3lem4 8888 axdc4lem 8890 axdclem2 8955 peano2nn 10628 om2uzrani 12173 uzrdgsuci 12181 fzennn 12188 axdc4uzlem 12202 bnj970 29770 trpredtr 30483 elhf2 30954 0hf 30956 hfsn 30958 hfpw 30964 neibastop2lem 31028 finxpsuclem 31801 |
Copyright terms: Public domain | W3C validator |