Theorem peano1 3782

Description: Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 3782 through peano5 3786 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity.

Assertion

Ref	Expression
peano1	|- (/) e. om

Proof of Theorem peano1

Step	Hyp	Ref	Expression
1		limom 3778	. 2 |- Lim om
2		0ellim 3541	. 2 |- (Lim om -> (/) e. om)
3	1, 2	ax-mp 7	1 |- (/) e. om

Syntax hints:   e. wcel 1138  (/)c0 2701  Lim wlim 3473  omcom 3760

This theorem is referenced by:  fr0g 4971  nnmcl 5094  nnmclOLD 5095  nnecl 5096  nneclOLD 5097  nnmsucr 5106  nnmsucrOLD 5107  1onn 5121  nneob 5123  snfi 5302  0sdom1dom 5428  infn0 5436  unblem2 5444  unfilem3 5453  unifi 5458  inf0 5521  infeq5 5536  axinf2 5539  dfom3 5546  noinfep 5556  trcl 5561  cardlim 5799  alephgeom 5826  alephfplem4 5843  mulclpi 5969  1lt2pi 5980  om2uzrani 7506  uzrdginii 7510  cardfz 7514  emfin 9959  bnj517 13051  trclpred 13726  top2usne 14618  fictb 15053  neibastop2lem4 15204  ufilen 15261  findcard2 15427

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761

Copyright terms: Public domain