![]() |
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 7232 through peano5 7236 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 7227 | . 2 ⊢ Lim ω | |
2 | 0ellim 5930 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 ∅c0 4063 Lim wlim 5867 ωcom 7212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pr 5034 ax-un 7096 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-tr 4887 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-om 7213 |
This theorem is referenced by: onnseq 7594 rdg0 7670 fr0g 7684 seqomlem3 7700 oa1suc 7765 om1 7776 oe1 7778 nna0r 7843 nnm0r 7844 nnmcl 7846 nnecl 7847 nnmsucr 7859 nnaword1 7863 nnaordex 7872 1onn 7873 oaabs2 7879 nnm1 7882 nneob 7886 omopth 7892 snfi 8194 0sdom1dom 8314 0fin 8344 findcard2 8356 nnunifi 8367 unblem2 8369 infn0 8378 unfilem3 8382 dffi3 8493 inf0 8682 infeq5i 8697 axinf2 8701 dfom3 8708 infdifsn 8718 noinfep 8721 cantnflt 8733 cnfcomlem 8760 cnfcom 8761 cnfcom2lem 8762 cnfcom3lem 8764 cnfcom3 8765 trcl 8768 rankdmr1 8828 rankeq0b 8887 cardlim 8998 infxpenc 9041 infxpenc2 9045 alephgeom 9105 alephfplem4 9130 ackbij1lem13 9256 ackbij1 9262 ackbij1b 9263 ominf4 9336 fin23lem16 9359 fin23lem31 9367 fin23lem40 9375 isf32lem9 9385 isf34lem7 9403 isf34lem6 9404 fin1a2lem6 9429 fin1a2lem7 9430 fin1a2lem11 9434 axdc3lem2 9475 axdc3lem4 9477 axdc4lem 9479 axcclem 9481 axdclem2 9544 pwfseqlem5 9687 omina 9715 wunex3 9765 1lt2pi 9929 1nn 11233 om2uzrani 12959 uzrdg0i 12966 fzennn 12975 axdc4uzlem 12990 hash1 13394 ltbwe 19687 2ndcdisj2 21481 snct 29831 trpredpred 32064 0hf 32621 neibastop2lem 32692 rdgeqoa 33555 finxp0 33565 cnfin0 33577 |
Copyright terms: Public domain | W3C validator |