Theorem peano1 4642

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 4171	. . . 4 |- (/) e. _V
2	1	elint 3891	. . 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 2192	. . . 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 1787	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2311	. . . . 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 1476	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4640	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2281	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1785   e. wcel 2176   {cab 2191   A.wral 2484   (/)c0 3460   |^|cint 3885   suc csuc 4412   omcom 4638

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-nul 4170

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168  df-nul 3461  df-int 3886  df-iom 4639

This theorem is referenced by:  peano5  4646  limom  4662  nnregexmid  4669  omsinds  4670  nnpredcl  4671  frec0g  6483  frecabcl  6485  frecrdg  6494  oa1suc  6553  nna0r  6564  nnm0r  6565  nnmcl  6567  nnmsucr  6574  1onn  6606  nnm1  6611  nnaordex  6614  nnawordex  6615  php5  6955  php5dom  6960  0fin  6981  findcard2  6986  findcard2s  6987  infm  7001  inffiexmid  7003  0ct  7209  ctmlemr  7210  ctssdclemn0  7212  ctssdc  7215  omct  7219  nninfisol  7235  fodjum  7248  fodju0  7249  ctssexmid  7252  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  1lt2pi  7453  nq0m0r  7569  nq0a0  7570  prarloclem5  7613  frec2uzrand  10550  frecuzrdg0  10558  frecuzrdg0t  10567  frecfzennn  10571  0tonninf  10585  1tonninf  10586  hashinfom  10923  hashunlem  10949  hash1  10956  nninfctlemfo  12361  ennnfonelemj0  12772  ennnfonelem1  12778  ennnfonelemhf1o  12784  ennnfonelemhom  12786  fnpr2o  13171  fvpr0o  13173  xpscf  13179  bj-nn0suc  15904  bj-nn0sucALT  15918  012of  15934  2o01f  15935  pwle2  15939  pwf1oexmid  15940  subctctexmid  15941  peano3nninf  15948  nninfall  15950  nninfsellemdc  15951  nninfsellemeq  15955  nninffeq  15961  nnnninfex  15963  isomninnlem  15973  iswomninnlem  15992  ismkvnnlem  15995