![]() |
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 7865 | . 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω) | |
2 | 1 | biimpi 215 | 1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 suc csuc 6356 ωcom 7848 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 ax-un 7718 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-tr 5256 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-om 7849 |
This theorem is referenced by: onnseq 8339 seqomlem1 8445 seqomlem4 8448 onasuc 8523 onmsuc 8524 onesuc 8525 o2p2e4 8536 nnacl 8606 nnecl 8608 nnacom 8612 nnmsucr 8620 1onnALT 8635 2onnALT 8637 3onn 8638 4onn 8639 nnneo 8649 nneob 8650 omopthlem1 8653 eldifsucnn 8658 findcard 9158 unfi 9167 phplem1 9202 php 9205 onomeneqOLD 9224 dif1ennnALT 9272 findcard2OLD 9279 unbnn2 9295 dffi3 9421 wofib 9535 axinf2 9630 dfom3 9637 noinfep 9650 cantnflt 9662 ttrcltr 9706 ttrclss 9710 ttrclselem2 9716 trcl 9718 cardsucnn 9975 harsucnn 9988 dif1card 10000 fseqdom 10016 alephfp 10098 ackbij1lem5 10214 ackbij1lem16 10225 ackbij2lem2 10230 ackbij2lem3 10231 ackbij2 10233 sornom 10267 infpssrlem4 10296 fin23lem26 10315 fin23lem20 10327 fin23lem38 10339 fin23lem39 10340 isf32lem2 10344 isf32lem3 10345 isf34lem7 10369 isf34lem6 10370 fin1a2lem6 10395 fin1a2lem9 10398 fin1a2lem12 10401 domtriomlem 10432 axdc2lem 10438 axdc3lem 10440 axdc3lem2 10441 axdc3lem4 10443 axdc4lem 10445 axdclem2 10510 peano2nn 12220 om2uzrani 13913 uzrdgsuci 13921 fzennn 13929 axdc4uzlem 13944 precsexlem4 28023 precsexlem5 28024 precsexlem11 28030 peano2n0s 28086 bnj970 34413 satfvsuc 34807 satfvsucsuc 34811 gonarlem 34840 goalrlem 34842 satffunlem2lem2 34852 satffunlem2 34854 ex-sategoelelomsuc 34872 elhf2 35608 0hf 35610 hfsn 35612 hfpw 35618 neibastop2lem 35701 exrecfnlem 36716 finxpsuclem 36734 domalom 36741 onexoegt 42448 nnoeomeqom 42517 nna1iscard 42751 |
Copyright terms: Public domain | W3C validator |