Theorem peano1 4686

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 4211	. . . 4 |- (/) e. _V
2	1	elint 3929	. . 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 2216	. . . 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 1810	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2335	. . . . 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 1499	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4684	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2305	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1808   e. wcel 2200   {cab 2215   A.wral 2508   (/)c0 3491   |^|cint 3923   suc csuc 4456   omcom 4682

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4210

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492  df-int 3924  df-iom 4683

This theorem is referenced by:  peano5  4690  limom  4706  nnregexmid  4713  omsinds  4714  nnpredcl  4715  frec0g  6543  frecabcl  6545  frecrdg  6554  oa1suc  6613  nna0r  6624  nnm0r  6625  nnmcl  6627  nnmsucr  6634  1onn  6666  nnm1  6671  nnaordex  6674  nnawordex  6675  php5  7019  php5dom  7024  0fin  7046  findcard2  7051  findcard2s  7052  infm  7066  inffiexmid  7068  0ct  7274  ctmlemr  7275  ctssdclemn0  7277  ctssdc  7280  omct  7284  nninfisol  7300  fodjum  7313  fodju0  7314  ctssexmid  7317  nninfwlpoimlemg  7342  nninfwlpoimlemginf  7343  1lt2pi  7527  nq0m0r  7643  nq0a0  7644  prarloclem5  7687  frec2uzrand  10627  frecuzrdg0  10635  frecuzrdg0t  10644  frecfzennn  10648  0tonninf  10662  1tonninf  10663  hashinfom  11000  hashunlem  11026  hash1  11033  nninfctlemfo  12561  ennnfonelemj0  12972  ennnfonelem1  12978  ennnfonelemhf1o  12984  ennnfonelemhom  12986  fnpr2o  13372  fvpr0o  13374  xpscf  13380  bj-nn0suc  16327  bj-nn0sucALT  16341  012of  16357  2o01f  16358  pwle2  16364  pwf1oexmid  16365  subctctexmid  16366  peano3nninf  16373  nninfall  16375  nninfsellemdc  16376  nninfsellemeq  16380  nninffeq  16386  nnnninfex  16388  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420