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 7596 | . 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | |
2 | 1 | biimpi 218 | 1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 suc csuc 6193 ωcom 7580 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-tr 5173 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-om 7581 |
This theorem is referenced by: onnseq 7981 seqomlem1 8086 seqomlem4 8089 onasuc 8153 onmsuc 8154 onesuc 8155 o2p2e4 8166 nnacl 8237 nnecl 8239 nnacom 8243 nnmsucr 8251 1onn 8265 2onn 8266 3onn 8267 4onn 8268 nnneo 8278 nneob 8279 omopthlem1 8282 onomeneq 8708 dif1en 8751 findcard 8757 findcard2 8758 unbnn2 8775 dffi3 8895 wofib 9009 axinf2 9103 dfom3 9110 noinfep 9123 cantnflt 9135 trcl 9170 cardsucnn 9414 dif1card 9436 fseqdom 9452 alephfp 9534 ackbij1lem5 9646 ackbij1lem16 9657 ackbij2lem2 9662 ackbij2lem3 9663 ackbij2 9665 sornom 9699 infpssrlem4 9728 fin23lem26 9747 fin23lem20 9759 fin23lem38 9771 fin23lem39 9772 isf32lem2 9776 isf32lem3 9777 isf34lem7 9801 isf34lem6 9802 fin1a2lem6 9827 fin1a2lem9 9830 fin1a2lem12 9833 domtriomlem 9864 axdc2lem 9870 axdc3lem 9872 axdc3lem2 9873 axdc3lem4 9875 axdc4lem 9877 axdclem2 9942 peano2nn 11650 om2uzrani 13321 uzrdgsuci 13329 fzennn 13337 axdc4uzlem 13352 bnj970 32219 satfvsuc 32608 satfvsucsuc 32612 gonarlem 32641 goalrlem 32643 satffunlem2lem2 32653 satffunlem2 32655 ex-sategoelelomsuc 32673 trpredtr 33069 elhf2 33636 0hf 33638 hfsn 33640 hfpw 33646 neibastop2lem 33708 exrecfnlem 34663 finxpsuclem 34681 domalom 34688 harsucnn 39923 |
Copyright terms: Public domain | W3C validator |