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  6563  frecabcl  6565  frecrdg  6574  oa1suc  6635  nna0r  6646  nnm0r  6647  nnmcl  6649  nnmsucr  6656  1onn  6688  nnm1  6693  nnaordex  6696  nnawordex  6697  php5  7044  php5dom  7049  0fi  7073  findcard2  7078  findcard2s  7079  infm  7096  inffiexmid  7098  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdc  7312  omct  7316  nninfisol  7332  fodjum  7345  fodju0  7346  ctssexmid  7349  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  1lt2pi  7560  nq0m0r  7676  nq0a0  7677  prarloclem5  7720  frec2uzrand  10667  frecuzrdg0  10675  frecuzrdg0t  10684  frecfzennn  10688  0tonninf  10702  1tonninf  10703  hashinfom  11040  hashunlem  11067  hash1  11075  nninfctlemfo  12612  ennnfonelemj0  13023  ennnfonelem1  13029  ennnfonelemhf1o  13035  ennnfonelemhom  13037  fnpr2o  13423  fvpr0o  13425  xpscf  13431  bj-nn0suc  16562  bj-nn0sucALT  16576  012of  16595  2o01f  16596  pwle2  16602  pwf1oexmid  16603  subctctexmid  16604  peano3nninf  16612  nninfall  16614  nninfsellemdc  16615  nninfsellemeq  16619  nninffeq  16625  nnnninfex  16627  isomninnlem  16637  iswomninnlem  16656  ismkvnnlem  16659