Theorem peano1 4587

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 4125	. . . 4 |- (/) e. _V
2	1	elint 3846	. . 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 2162	. . . 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 1762	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2281	. . . . 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 1451	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4585	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2251	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1760   e. wcel 2146   {cab 2161   A.wral 2453   (/)c0 3420   |^|cint 3840   suc csuc 4359   omcom 4583

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-nul 4124

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-dif 3129  df-nul 3421  df-int 3841  df-iom 4584

This theorem is referenced by:  peano5  4591  limom  4607  nnregexmid  4614  omsinds  4615  nnpredcl  4616  frec0g  6388  frecabcl  6390  frecrdg  6399  oa1suc  6458  nna0r  6469  nnm0r  6470  nnmcl  6472  nnmsucr  6479  1onn  6511  nnm1  6516  nnaordex  6519  nnawordex  6520  php5  6848  php5dom  6853  0fin  6874  findcard2  6879  findcard2s  6880  infm  6894  inffiexmid  6896  0ct  7096  ctmlemr  7097  ctssdclemn0  7099  ctssdc  7102  omct  7106  nninfisol  7121  fodjum  7134  fodju0  7135  ctssexmid  7138  nninfwlpoimlemg  7163  nninfwlpoimlemginf  7164  1lt2pi  7314  nq0m0r  7430  nq0a0  7431  prarloclem5  7474  frec2uzrand  10375  frecuzrdg0  10383  frecuzrdg0t  10392  frecfzennn  10396  0tonninf  10409  1tonninf  10410  hashinfom  10726  hashunlem  10752  hash1  10759  ennnfonelemj0  12369  ennnfonelem1  12375  ennnfonelemhf1o  12381  ennnfonelemhom  12383  bj-nn0suc  14285  bj-nn0sucALT  14299  012of  14314  2o01f  14315  pwle2  14317  pwf1oexmid  14318  subctctexmid  14320  peano3nninf  14326  nninfall  14328  nninfsellemdc  14329  nninfsellemeq  14333  nninffeq  14339  isomninnlem  14348  iswomninnlem  14367  ismkvnnlem  14370