| 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 7910 through peano5 7915 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.) Avoid ax-un 7755. (Revised by BTernaryTau, 29-Nov-2024.) |
| Ref | Expression |
|---|---|
| peano1 | ⊢ ∅ ∈ ω |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0elon 6438 | . 2 ⊢ ∅ ∈ On | |
| 2 | 0ellim 6447 | . . 3 ⊢ (Lim 𝑥 → ∅ ∈ 𝑥) | |
| 3 | 2 | ax-gen 1795 | . 2 ⊢ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥) |
| 4 | elom 7890 | . 2 ⊢ (∅ ∈ ω ↔ (∅ ∈ On ∧ ∀𝑥(Lim 𝑥 → ∅ ∈ 𝑥))) | |
| 5 | 1, 3, 4 | mpbir2an 711 | 1 ⊢ ∅ ∈ ω |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∈ wcel 2108 ∅c0 4333 Oncon0 6384 Lim wlim 6385 ωcom 7887 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 df-lim 6389 df-om 7888 |
| This theorem is referenced by: onnseq 8384 rdg0 8461 fr0g 8476 seqomlem3 8492 oa1suc 8569 o2p2e4 8579 om1 8580 oe1 8582 nna0r 8647 nnm0r 8648 nnmcl 8650 nnecl 8651 nnmsucr 8663 nnaword1 8667 nnaordex 8676 1onnALT 8679 oaabs2 8687 nnm1 8690 nneob 8694 omopth 8700 0fi 9082 snfiOLD 9084 0finOLD 9210 0sdom1domALT 9275 isinf 9296 nnunifi 9327 unblem2 9329 infn0 9340 infn0ALT 9341 unfilem3 9345 dffi3 9471 inf0 9661 infeq5i 9676 axinf2 9680 dfom3 9687 infdifsn 9697 noinfep 9700 cantnflt 9712 cnfcomlem 9739 cnfcom 9740 cnfcom2lem 9741 cnfcom3lem 9743 cnfcom3 9744 brttrcl2 9754 ttrcltr 9756 rnttrcl 9762 trcl 9768 rankdmr1 9841 rankeq0b 9900 cardlim 10012 infxpenc 10058 infxpenc2 10062 alephgeom 10122 alephfplem4 10147 ackbij1lem13 10271 ackbij1 10277 ackbij1b 10278 ominf4 10352 fin23lem16 10375 fin23lem31 10383 fin23lem40 10391 isf32lem9 10401 isf34lem7 10419 isf34lem6 10420 fin1a2lem6 10445 fin1a2lem7 10446 fin1a2lem11 10450 axdc3lem2 10491 axdc3lem4 10493 axdc4lem 10495 axcclem 10497 axdclem2 10560 pwfseqlem5 10703 omina 10731 wunex3 10781 1lt2pi 10945 1nn 12277 om2uzrani 13993 uzrdg0i 14000 fzennn 14009 axdc4uzlem 14024 hash1 14443 fnpr2o 17602 fvpr0o 17604 ltbwe 22062 2ndcdisj2 23465 precsexlem11 28241 noseq0 28296 noseqrdg0 28313 n0sbday 28354 dfnns2 28362 snct 32725 goelel3xp 35353 satfv0 35363 satfv1 35368 satf0 35377 satf00 35379 satf0suclem 35380 sat1el2xp 35384 fmla0 35387 fmlasuc0 35389 fmla1 35392 gonan0 35397 gonar 35400 goalr 35402 satffunlem1lem2 35408 satffunlem1 35412 satefvfmla0 35423 prv0 35435 nnuni 35727 0hf 36178 neibastop2lem 36361 bj-rdg0gALT 37072 rdgeqoa 37371 exrecfnlem 37380 finxp0 37392 onexomgt 43253 onexoegt 43256 omnord1 43318 oenord1 43329 oaomoencom 43330 cantnftermord 43333 cantnfub 43334 cantnf2 43338 dflim5 43342 oacl2g 43343 onmcl 43344 omabs2 43345 omcl2 43346 tfsconcat0b 43359 ofoaf 43368 ofoafo 43369 ofoaid1 43371 ofoaid2 43372 naddcnff 43375 naddcnffo 43377 naddcnfid1 43380 naddcnfid2 43381 0finon 43461 0iscard 43554 omssaxinf2 45005 |
| Copyright terms: Public domain | W3C validator |