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  6549  frecabcl  6551  frecrdg  6560  oa1suc  6621  nna0r  6632  nnm0r  6633  nnmcl  6635  nnmsucr  6642  1onn  6674  nnm1  6679  nnaordex  6682  nnawordex  6683  php5  7027  php5dom  7032  0fi  7054  findcard2  7059  findcard2s  7060  infm  7077  inffiexmid  7079  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  omct  7295  nninfisol  7311  fodjum  7324  fodju0  7325  ctssexmid  7328  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  1lt2pi  7538  nq0m0r  7654  nq0a0  7655  prarloclem5  7698  frec2uzrand  10639  frecuzrdg0  10647  frecuzrdg0t  10656  frecfzennn  10660  0tonninf  10674  1tonninf  10675  hashinfom  11012  hashunlem  11038  hash1  11046  nninfctlemfo  12577  ennnfonelemj0  12988  ennnfonelem1  12994  ennnfonelemhf1o  13000  ennnfonelemhom  13002  fnpr2o  13388  fvpr0o  13390  xpscf  13396  bj-nn0suc  16410  bj-nn0sucALT  16424  012of  16444  2o01f  16445  pwle2  16451  pwf1oexmid  16452  subctctexmid  16453  peano3nninf  16461  nninfall  16463  nninfsellemdc  16464  nninfsellemeq  16468  nninffeq  16474  nnnninfex  16476  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508