Theorem peano1 4627

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 4157	. . . 4 |- (/) e. _V
2	1	elint 3877	. . 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 2180	. . . 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 1775	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2299	. . . . 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 1464	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4625	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2269	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1773   e. wcel 2164   {cab 2179   A.wral 2472   (/)c0 3447   |^|cint 3871   suc csuc 4397   omcom 4623

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-nul 4156

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3156  df-nul 3448  df-int 3872  df-iom 4624

This theorem is referenced by:  peano5  4631  limom  4647  nnregexmid  4654  omsinds  4655  nnpredcl  4656  frec0g  6452  frecabcl  6454  frecrdg  6463  oa1suc  6522  nna0r  6533  nnm0r  6534  nnmcl  6536  nnmsucr  6543  1onn  6575  nnm1  6580  nnaordex  6583  nnawordex  6584  php5  6916  php5dom  6921  0fin  6942  findcard2  6947  findcard2s  6948  infm  6962  inffiexmid  6964  0ct  7168  ctmlemr  7169  ctssdclemn0  7171  ctssdc  7174  omct  7178  nninfisol  7194  fodjum  7207  fodju0  7208  ctssexmid  7211  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  1lt2pi  7402  nq0m0r  7518  nq0a0  7519  prarloclem5  7562  frec2uzrand  10479  frecuzrdg0  10487  frecuzrdg0t  10496  frecfzennn  10500  0tonninf  10514  1tonninf  10515  hashinfom  10852  hashunlem  10878  hash1  10885  nninfctlemfo  12180  ennnfonelemj0  12561  ennnfonelem1  12567  ennnfonelemhf1o  12573  ennnfonelemhom  12575  fnpr2o  12925  fvpr0o  12927  xpscf  12933  bj-nn0suc  15526  bj-nn0sucALT  15540  012of  15556  2o01f  15557  pwle2  15559  pwf1oexmid  15560  subctctexmid  15561  peano3nninf  15567  nninfall  15569  nninfsellemdc  15570  nninfsellemeq  15574  nninffeq  15580  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612