Theorem peano1 4643

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 4172	. . . 4 |- (/) e. _V
2	1	elint 3891	. . 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 2192	. . . 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 1787	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2311	. . . . 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 1476	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4641	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2281	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 104   [wsb 1785   e. wcel 2176   {cab 2191   A.wral 2484   (/)c0 3460   |^|cint 3885   suc csuc 4413   omcom 4639

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-nul 4171

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168  df-nul 3461  df-int 3886  df-iom 4640

This theorem is referenced by:  peano5  4647  limom  4663  nnregexmid  4670  omsinds  4671  nnpredcl  4672  frec0g  6485  frecabcl  6487  frecrdg  6496  oa1suc  6555  nna0r  6566  nnm0r  6567  nnmcl  6569  nnmsucr  6576  1onn  6608  nnm1  6613  nnaordex  6616  nnawordex  6617  php5  6957  php5dom  6962  0fin  6983  findcard2  6988  findcard2s  6989  infm  7003  inffiexmid  7005  0ct  7211  ctmlemr  7212  ctssdclemn0  7214  ctssdc  7217  omct  7221  nninfisol  7237  fodjum  7250  fodju0  7251  ctssexmid  7254  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  1lt2pi  7455  nq0m0r  7571  nq0a0  7572  prarloclem5  7615  frec2uzrand  10552  frecuzrdg0  10560  frecuzrdg0t  10569  frecfzennn  10573  0tonninf  10587  1tonninf  10588  hashinfom  10925  hashunlem  10951  hash1  10958  nninfctlemfo  12394  ennnfonelemj0  12805  ennnfonelem1  12811  ennnfonelemhf1o  12817  ennnfonelemhom  12819  fnpr2o  13204  fvpr0o  13206  xpscf  13212  bj-nn0suc  15937  bj-nn0sucALT  15951  012of  15967  2o01f  15968  pwle2  15972  pwf1oexmid  15973  subctctexmid  15974  peano3nninf  15981  nninfall  15983  nninfsellemdc  15984  nninfsellemeq  15988  nninffeq  15994  nnnninfex  15996  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028