![]() |
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 7363 through peano5 7367 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 7358 | . 2 ⊢ Lim ω | |
2 | 0ellim 6038 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ∅c0 4141 Lim wlim 5977 ωcom 7343 |
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 5017 ax-nul 5025 ax-pr 5138 ax-un 7226 |
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 4672 df-br 4887 df-opab 4949 df-tr 4988 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-we 5316 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-om 7344 |
This theorem is referenced by: onnseq 7724 rdg0 7800 fr0g 7814 seqomlem3 7830 oa1suc 7895 om1 7906 oe1 7908 nna0r 7973 nnm0r 7974 nnmcl 7976 nnecl 7977 nnmsucr 7989 nnaword1 7993 nnaordex 8002 1onn 8003 oaabs2 8009 nnm1 8012 nneob 8016 omopth 8022 snfi 8326 0sdom1dom 8446 0fin 8476 findcard2 8488 nnunifi 8499 unblem2 8501 infn0 8510 unfilem3 8514 dffi3 8625 inf0 8815 infeq5i 8830 axinf2 8834 dfom3 8841 infdifsn 8851 noinfep 8854 cantnflt 8866 cnfcomlem 8893 cnfcom 8894 cnfcom2lem 8895 cnfcom3lem 8897 cnfcom3 8898 trcl 8901 rankdmr1 8961 rankeq0b 9020 cardlim 9131 infxpenc 9174 infxpenc2 9178 alephgeom 9238 alephfplem4 9263 ackbij1lem13 9389 ackbij1 9395 ackbij1b 9396 ominf4 9469 fin23lem16 9492 fin23lem31 9500 fin23lem40 9508 isf32lem9 9518 isf34lem7 9536 isf34lem6 9537 fin1a2lem6 9562 fin1a2lem7 9563 fin1a2lem11 9567 axdc3lem2 9608 axdc3lem4 9610 axdc4lem 9612 axcclem 9614 axdclem2 9677 pwfseqlem5 9820 omina 9848 wunex3 9898 1lt2pi 10062 1nn 11387 om2uzrani 13070 uzrdg0i 13077 fzennn 13086 axdc4uzlem 13101 hash1 13506 ltbwe 19869 2ndcdisj2 21669 snct 30057 trpredpred 32316 0hf 32873 neibastop2lem 32943 rdgeqoa 33813 finxp0 33823 cnfin0 33835 |
Copyright terms: Public domain | W3C validator |