Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > peano1 | Structured version Visualization version GIF version |
Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7723 through peano5 7727 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) |
Ref | Expression |
---|---|
peano1 | ⊢ ∅ ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limom 7716 | . 2 ⊢ Lim ω | |
2 | 0ellim 6325 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2109 ∅c0 4261 Lim wlim 6264 ωcom 7700 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-11 2157 ax-ext 2710 ax-sep 5226 ax-nul 5233 ax-pr 5355 ax-un 7579 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-sb 2071 df-clab 2717 df-cleq 2731 df-clel 2817 df-ne 2945 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3432 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4845 df-br 5079 df-opab 5141 df-tr 5196 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-we 5545 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-om 7701 |
This theorem is referenced by: onnseq 8159 rdg0 8236 fr0g 8251 seqomlem3 8267 oa1suc 8337 o2p2e4 8347 om1 8349 oe1 8351 nna0r 8416 nnm0r 8417 nnmcl 8419 nnecl 8420 nnmsucr 8432 nnaword1 8436 nnaordex 8445 1onn 8446 oaabs2 8453 nnm1 8456 nneob 8460 omopth 8466 snfi 8804 0fin 8919 0sdom1dom 8982 findcard2OLD 9017 nnunifi 9026 unblem2 9028 infn0 9037 unfilem3 9041 dffi3 9151 inf0 9340 infeq5i 9355 axinf2 9359 dfom3 9366 infdifsn 9376 noinfep 9379 cantnflt 9391 cnfcomlem 9418 cnfcom 9419 cnfcom2lem 9420 cnfcom3lem 9422 cnfcom3 9423 brttrcl2 9433 ttrcltr 9435 rnttrcl 9441 trpredpred 9458 trcl 9469 rankdmr1 9543 rankeq0b 9602 cardlim 9714 infxpenc 9758 infxpenc2 9762 alephgeom 9822 alephfplem4 9847 ackbij1lem13 9972 ackbij1 9978 ackbij1b 9979 ominf4 10052 fin23lem16 10075 fin23lem31 10083 fin23lem40 10091 isf32lem9 10101 isf34lem7 10119 isf34lem6 10120 fin1a2lem6 10145 fin1a2lem7 10146 fin1a2lem11 10150 axdc3lem2 10191 axdc3lem4 10193 axdc4lem 10195 axcclem 10197 axdclem2 10260 pwfseqlem5 10403 omina 10431 wunex3 10481 1lt2pi 10645 1nn 11967 om2uzrani 13653 uzrdg0i 13660 fzennn 13669 axdc4uzlem 13684 hash1 14100 fnpr2o 17249 fvpr0o 17251 ltbwe 21226 2ndcdisj2 22589 snct 31027 goelel3xp 33289 satfv0 33299 satfv1 33304 satf0 33313 satf00 33315 satf0suclem 33316 sat1el2xp 33320 fmla0 33323 fmlasuc0 33325 fmla1 33328 gonan0 33333 gonar 33336 goalr 33338 satffunlem1lem2 33344 satffunlem1 33348 satefvfmla0 33359 prv0 33371 nnuni 33671 0hf 34458 neibastop2lem 34528 bj-rdg0gALT 35221 rdgeqoa 35520 exrecfnlem 35529 finxp0 35541 |
Copyright terms: Public domain | W3C validator |