Theorem peano1 4660

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 4187	. . . 4 |- (/) e. _V
2	1	elint 3905	. . 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 2194	. . . 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 1788	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2313	. . . . 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 1477	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4658	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2283	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1786   e. wcel 2178   {cab 2193   A.wral 2486   (/)c0 3468   |^|cint 3899   suc csuc 4430   omcom 4656

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-nul 4186

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-dif 3176  df-nul 3469  df-int 3900  df-iom 4657

This theorem is referenced by:  peano5  4664  limom  4680  nnregexmid  4687  omsinds  4688  nnpredcl  4689  frec0g  6506  frecabcl  6508  frecrdg  6517  oa1suc  6576  nna0r  6587  nnm0r  6588  nnmcl  6590  nnmsucr  6597  1onn  6629  nnm1  6634  nnaordex  6637  nnawordex  6638  php5  6980  php5dom  6985  0fin  7007  findcard2  7012  findcard2s  7013  infm  7027  inffiexmid  7029  0ct  7235  ctmlemr  7236  ctssdclemn0  7238  ctssdc  7241  omct  7245  nninfisol  7261  fodjum  7274  fodju0  7275  ctssexmid  7278  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  1lt2pi  7488  nq0m0r  7604  nq0a0  7605  prarloclem5  7648  frec2uzrand  10587  frecuzrdg0  10595  frecuzrdg0t  10604  frecfzennn  10608  0tonninf  10622  1tonninf  10623  hashinfom  10960  hashunlem  10986  hash1  10993  nninfctlemfo  12476  ennnfonelemj0  12887  ennnfonelem1  12893  ennnfonelemhf1o  12899  ennnfonelemhom  12901  fnpr2o  13286  fvpr0o  13288  xpscf  13294  bj-nn0suc  16099  bj-nn0sucALT  16113  012of  16130  2o01f  16131  pwle2  16137  pwf1oexmid  16138  subctctexmid  16139  peano3nninf  16146  nninfall  16148  nninfsellemdc  16149  nninfsellemeq  16153  nninffeq  16159  nnnninfex  16161  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193