Theorem peano1 4466

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 4013	. . . 4 |- (/) e. _V
2	1	elint 3741	. . 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 2100	. . . 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 108	. . . . . 6 |- ( ( (/) e. y /\ A. x e. y suc x e. y ) -> (/) e. y )
5	4	sbimi 1718	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb4 2218	. . . . 5 |- ( [ z / y ] (/) e. y <-> (/) e. z )
7	5, 6	sylib 121	. . . 4 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> (/) e. z )
8	3, 7	sylbi 120	. . 3 |- ( z e. { y | ( (/) e. y /\ A. x e. y suc x e. y ) } -> (/) e. z )
9	2, 8	mpgbir 1410	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4464	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2188	1 |- (/) e. om

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1461   [wsb 1716   {cab 2099   A.wral 2388   (/)c0 3327   |^|cint 3735   suc csuc 4245   omcom 4462

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-nul 4012

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-dif 3037  df-nul 3328  df-int 3736  df-iom 4463

This theorem is referenced by:  peano5  4470  limom  4485  nnregexmid  4492  omsinds  4493  nnpredcl  4494  frec0g  6245  frecabcl  6247  frecrdg  6256  oa1suc  6314  nna0r  6325  nnm0r  6326  nnmcl  6328  nnmsucr  6335  1onn  6367  nnm1  6371  nnaordex  6374  nnawordex  6375  php5  6702  php5dom  6707  0fin  6728  findcard2  6733  findcard2s  6734  infm  6748  inffiexmid  6750  0ct  6941  ctmlemr  6942  ctssdclemn0  6944  ctssdc  6947  fodjum  6965  fodju0  6966  ctssexmid  6971  1lt2pi  7089  nq0m0r  7205  nq0a0  7206  prarloclem5  7249  frec2uzrand  10064  frecuzrdg0  10072  frecuzrdg0t  10081  frecfzennn  10085  0tonninf  10098  1tonninf  10099  hashinfom  10410  hashunlem  10436  hash1  10443  ennnfonelemj0  11752  ennnfonelem1  11758  ennnfonelemhf1o  11764  ennnfonelemhom  11766  bj-nn0suc  12841  bj-nn0sucALT  12855  pwle2  12872  pwf1oexmid  12873  peano3nninf  12878  nninfall  12881  nninfsellemdc  12883  nninfsellemeq  12887  nninffeq  12893  isomninnlem  12902