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 6977 through peano5 6981 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 6972 | . 2 ⊢ Lim ω | |
2 | 0ellim 5704 | . 2 ⊢ (Lim ω → ∅ ∈ ω) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∅ ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 ∅c0 3874 Lim wlim 5641 ωcom 6957 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-tr 4681 df-eprel 4949 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-om 6958 |
This theorem is referenced by: onnseq 7328 rdg0 7404 fr0g 7418 seqomlem3 7434 oa1suc 7498 om1 7509 oe1 7511 nna0r 7576 nnm0r 7577 nnmcl 7579 nnecl 7580 nnmsucr 7592 nnaword1 7596 nnaordex 7605 1onn 7606 oaabs2 7612 nnm1 7615 nneob 7619 omopth 7625 snfi 7923 0sdom1dom 8043 0fin 8073 findcard2 8085 nnunifi 8096 unblem2 8098 infn0 8107 unfilem3 8111 dffi3 8220 inf0 8401 infeq5i 8416 axinf2 8420 dfom3 8427 infdifsn 8437 noinfep 8440 cantnflt 8452 cnfcomlem 8479 cnfcom 8480 cnfcom2lem 8481 cnfcom3lem 8483 cnfcom3 8484 trcl 8487 rankdmr1 8547 rankeq0b 8606 cardlim 8681 infxpenc 8724 infxpenc2 8728 alephgeom 8788 alephfplem4 8813 ackbij1lem13 8937 ackbij1 8943 ackbij1b 8944 ominf4 9017 fin23lem16 9040 fin23lem31 9048 fin23lem40 9056 isf32lem9 9066 isf34lem7 9084 isf34lem6 9085 fin1a2lem6 9110 fin1a2lem7 9111 fin1a2lem11 9115 axdc3lem2 9156 axdc3lem4 9158 axdc4lem 9160 axcclem 9162 axdclem2 9225 pwfseqlem5 9364 omina 9392 wunex3 9442 1lt2pi 9606 1nn 10908 om2uzrani 12613 uzrdg0i 12620 fzennn 12629 axdc4uzlem 12644 hash1 13053 ltbwe 19293 2ndcdisj2 21070 snct 28874 trpredpred 30972 0hf 31454 neibastop2lem 31525 rdgeqoa 32394 finxp0 32404 |
Copyright terms: Public domain | W3C validator |