Theorem peano1 4692

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 4216	. . . 4 |- (/) e. _V
2	1	elint 3934	. . 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 1501	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4690	. 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 2510   (/)c0 3494   |^|cint 3928   suc csuc 4462   omcom 4688

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-nul 4215

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-nul 3495  df-int 3929  df-iom 4689

This theorem is referenced by:  peano5  4696  limom  4712  nnregexmid  4719  omsinds  4720  nnpredcl  4721  frec0g  6566  frecabcl  6568  frecrdg  6577  oa1suc  6638  nna0r  6649  nnm0r  6650  nnmcl  6652  nnmsucr  6659  1onn  6691  nnm1  6696  nnaordex  6699  nnawordex  6700  php5  7047  php5dom  7052  0fi  7076  findcard2  7081  findcard2s  7082  infm  7099  inffiexmid  7101  0ct  7309  ctmlemr  7310  ctssdclemn0  7312  ctssdc  7315  omct  7319  nninfisol  7335  fodjum  7348  fodju0  7349  ctssexmid  7352  nninfwlpoimlemg  7377  nninfwlpoimlemginf  7378  1lt2pi  7563  nq0m0r  7679  nq0a0  7680  prarloclem5  7723  frec2uzrand  10671  frecuzrdg0  10679  frecuzrdg0t  10688  frecfzennn  10692  0tonninf  10706  1tonninf  10707  hashinfom  11044  hashunlem  11071  hash1  11079  nninfctlemfo  12632  ennnfonelemj0  13043  ennnfonelem1  13049  ennnfonelemhf1o  13055  ennnfonelemhom  13057  fnpr2o  13443  fvpr0o  13445  xpscf  13451  bj-nn0suc  16618  bj-nn0sucALT  16632  012of  16651  2o01f  16652  pwle2  16658  pwf1oexmid  16659  subctctexmid  16660  peano3nninf  16668  nninfall  16670  nninfsellemdc  16671  nninfsellemeq  16675  nninffeq  16681  nnnninfex  16683  isomninnlem  16693  iswomninnlem  16713  ismkvnnlem  16716