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 7581 through peano5 7585 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 7575 | . 2 ⊢ Lim ω | |
2 | 0ellim 6221 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 ∅c0 4243 Lim wlim 6160 ωcom 7560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-om 7561 |
This theorem is referenced by: onnseq 7964 rdg0 8040 fr0g 8054 seqomlem3 8071 oa1suc 8139 o2p2e4 8149 om1 8151 oe1 8153 nna0r 8218 nnm0r 8219 nnmcl 8221 nnecl 8222 nnmsucr 8234 nnaword1 8238 nnaordex 8247 1onn 8248 oaabs2 8255 nnm1 8258 nneob 8262 omopth 8268 snfi 8577 0sdom1dom 8700 0fin 8730 findcard2 8742 nnunifi 8753 unblem2 8755 infn0 8764 unfilem3 8768 dffi3 8879 inf0 9068 infeq5i 9083 axinf2 9087 dfom3 9094 infdifsn 9104 noinfep 9107 cantnflt 9119 cnfcomlem 9146 cnfcom 9147 cnfcom2lem 9148 cnfcom3lem 9150 cnfcom3 9151 trcl 9154 rankdmr1 9214 rankeq0b 9273 cardlim 9385 infxpenc 9429 infxpenc2 9433 alephgeom 9493 alephfplem4 9518 ackbij1lem13 9643 ackbij1 9649 ackbij1b 9650 ominf4 9723 fin23lem16 9746 fin23lem31 9754 fin23lem40 9762 isf32lem9 9772 isf34lem7 9790 isf34lem6 9791 fin1a2lem6 9816 fin1a2lem7 9817 fin1a2lem11 9821 axdc3lem2 9862 axdc3lem4 9864 axdc4lem 9866 axcclem 9868 axdclem2 9931 pwfseqlem5 10074 omina 10102 wunex3 10152 1lt2pi 10316 1nn 11636 om2uzrani 13315 uzrdg0i 13322 fzennn 13331 axdc4uzlem 13346 hash1 13761 fnpr2o 16822 fvpr0o 16824 ltbwe 20712 2ndcdisj2 22062 snct 30475 goelel3xp 32708 satfv0 32718 satfv1 32723 satf0 32732 satf00 32734 satf0suclem 32735 sat1el2xp 32739 fmla0 32742 fmlasuc0 32744 fmla1 32747 gonan0 32752 gonar 32755 goalr 32757 satffunlem1lem2 32763 satffunlem1 32767 satefvfmla0 32778 prv0 32790 trpredpred 33180 0hf 33751 neibastop2lem 33821 rdgeqoa 34787 exrecfnlem 34796 finxp0 34808 |
Copyright terms: Public domain | W3C validator |