![]() |
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 7365 through peano5 7369 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 7360 | . 2 ⊢ Lim ω | |
2 | 0ellim 6040 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ∅c0 4141 Lim wlim 5979 ωcom 7345 |
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 5019 ax-nul 5027 ax-pr 5140 ax-un 7228 |
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 4674 df-br 4889 df-opab 4951 df-tr 4990 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 df-om 7346 |
This theorem is referenced by: onnseq 7726 rdg0 7802 fr0g 7816 seqomlem3 7832 oa1suc 7897 om1 7908 oe1 7910 nna0r 7975 nnm0r 7976 nnmcl 7978 nnecl 7979 nnmsucr 7991 nnaword1 7995 nnaordex 8004 1onn 8005 oaabs2 8011 nnm1 8014 nneob 8018 omopth 8024 snfi 8328 0sdom1dom 8448 0fin 8478 findcard2 8490 nnunifi 8501 unblem2 8503 infn0 8512 unfilem3 8516 dffi3 8627 inf0 8817 infeq5i 8832 axinf2 8836 dfom3 8843 infdifsn 8853 noinfep 8856 cantnflt 8868 cnfcomlem 8895 cnfcom 8896 cnfcom2lem 8897 cnfcom3lem 8899 cnfcom3 8900 trcl 8903 rankdmr1 8963 rankeq0b 9022 cardlim 9133 infxpenc 9176 infxpenc2 9180 alephgeom 9240 alephfplem4 9265 ackbij1lem13 9391 ackbij1 9397 ackbij1b 9398 ominf4 9471 fin23lem16 9494 fin23lem31 9502 fin23lem40 9510 isf32lem9 9520 isf34lem7 9538 isf34lem6 9539 fin1a2lem6 9564 fin1a2lem7 9565 fin1a2lem11 9569 axdc3lem2 9610 axdc3lem4 9612 axdc4lem 9614 axcclem 9616 axdclem2 9679 pwfseqlem5 9822 omina 9850 wunex3 9900 1lt2pi 10064 1nn 11392 om2uzrani 13075 uzrdg0i 13082 fzennn 13091 axdc4uzlem 13106 hash1 13512 ltbwe 19880 2ndcdisj2 21680 snct 30074 trpredpred 32324 0hf 32881 neibastop2lem 32951 rdgeqoa 33820 finxp0 33830 cnfin0 33842 |
Copyright terms: Public domain | W3C validator |