Theorem peano1 4698

Description: Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. (Contributed by NM, 15-May-1994.)

Assertion

Ref	Expression
peano1	|- (/) e. om

Proof of Theorem peano1

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4221	. . . 4 |- (/) e. _V
2	1	elint 3939	. . 3 |- ( (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> A. z ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> (/) e. z ) )
3		df-clab 2218	. . . 4 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } <-> [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) )
4		simpl 109	. . . . . 6 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> (/) e. y )
5	4	sbimi 1812	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2337	. . . . 5 |- ( [ z / y ] (/) e. y <-> (/) e. z )
7	5, 6	sylib 122	. . . 4 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> (/) e. z )
8	3, 7	sylbi 121	. . 3 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> (/) e. z )
9	2, 8	mpgbir 1502	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4696	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2307	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1810   e. wcel 2202   {cab 2217   A.wral 2511   (/)c0 3496   |^|cint 3933   suc csuc 4468   omcom 4694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-nul 3497  df-int 3934  df-iom 4695

This theorem is referenced by:  peano5  4702  limom  4718  nnregexmid  4725  omsinds  4726  nnpredcl  4727  frec0g  6606  frecabcl  6608  frecrdg  6617  oa1suc  6678  nna0r  6689  nnm0r  6690  nnmcl  6692  nnmsucr  6699  1onn  6731  nnm1  6736  nnaordex  6739  nnawordex  6740  php5  7087  php5dom  7092  0fi  7116  findcard2  7121  findcard2s  7122  infm  7139  inffiexmid  7141  0ct  7366  ctmlemr  7367  ctssdclemn0  7369  ctssdc  7372  omct  7376  nninfisol  7392  fodjum  7405  fodju0  7406  ctssexmid  7409  nninfwlpoimlemg  7434  nninfwlpoimlemginf  7435  1lt2pi  7620  nq0m0r  7736  nq0a0  7737  prarloclem5  7780  frec2uzrand  10730  frecuzrdg0  10738  frecuzrdg0t  10747  frecfzennn  10751  0tonninf  10765  1tonninf  10766  hashinfom  11103  hashunlem  11130  hash1  11138  nninfctlemfo  12691  ennnfonelemj0  13102  ennnfonelem1  13108  ennnfonelemhf1o  13114  ennnfonelemhom  13116  fnpr2o  13502  fvpr0o  13504  xpscf  13510  bj-nn0suc  16680  bj-nn0sucALT  16694  012of  16713  2o01f  16714  pwle2  16720  pwf1oexmid  16721  subctctexmid  16722  peano3nninf  16733  nninfall  16735  nninfsellemdc  16736  nninfsellemeq  16740  nninffeq  16746  nnnninfex  16748  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785