![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > peano2 | Structured version Visualization version GIF 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 | ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano2b 7361 | . 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | |
2 | 1 | biimpi 208 | 1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 suc csuc 5980 ωcom 7345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-tr 4990 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 df-om 7346 |
This theorem is referenced by: onnseq 7726 seqomlem1 7830 seqomlem4 7833 onasuc 7894 onmsuc 7895 onesuc 7896 nnacl 7977 nnecl 7979 nnacom 7983 nnmsucr 7991 1onn 8005 2onn 8006 3onn 8007 4onn 8008 nnneo 8017 nneob 8018 omopthlem1 8021 onomeneq 8440 dif1en 8483 findcard 8489 findcard2 8490 unbnn2 8507 dffi3 8627 wofib 8741 axinf2 8836 dfom3 8843 noinfep 8856 cantnflt 8868 trcl 8903 cardsucnn 9146 dif1card 9168 fseqdom 9184 alephfp 9266 ackbij1lem5 9383 ackbij1lem16 9394 ackbij2lem2 9399 ackbij2lem3 9400 ackbij2 9402 sornom 9436 infpssrlem4 9465 fin23lem26 9484 fin23lem20 9496 fin23lem38 9508 fin23lem39 9509 isf32lem2 9513 isf32lem3 9514 isf34lem7 9538 isf34lem6 9539 fin1a2lem6 9564 fin1a2lem9 9567 fin1a2lem12 9570 domtriomlem 9601 axdc2lem 9607 axdc3lem 9609 axdc3lem2 9610 axdc3lem4 9612 axdc4lem 9614 axdclem2 9679 peano2nn 11392 om2uzrani 13074 uzrdgsuci 13082 fzennn 13090 axdc4uzlem 13105 bnj970 31620 trpredtr 32322 elhf2 32875 0hf 32877 hfsn 32879 hfpw 32885 neibastop2lem 32947 finxpsuclem 33832 |
Copyright terms: Public domain | W3C validator |