Theorem peano1 4743

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 4262	. . . 4 |- (/) e. _V
2	1	elint 3976	. . 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 2225	. . . 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 1817	. . . . 5 |- ( [ z / y ] ( (/) e. y /\ A. x e. y suc x e. y ) -> [ z / y ] (/) e. y )
6		clelsb2 2344	. . . . 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 1506	. 2 |- (/) e. |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
10		dfom3 4741	. 2 |- om = |^| { y | ( (/) e. y /\ A. x e. y suc x e. y ) }
11	9, 10	eleqtrri 2314	1 |- (/) e. om

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   [wsb 1815   e. wcel 2209   {cab 2224   A.wral 2528   (/)c0 3520   |^|cint 3970   suc csuc 4512   omcom 4739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4261

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-nul 3521  df-int 3971  df-iom 4740

This theorem is used by:  peano5  4747  limom  4763  nnregexmid  4770  omsinds  4771  nnpredcl  4772  frec0g  6672  frecabcl  6674  frecrdg  6683  oa1suc  6744  nna0r  6755  nnm0r  6756  nnmcl  6758  nnmsucr  6765  1onn  6797  nnm1  6802  nnaordex  6805  nnawordex  6806  php5  7163  php5dom  7168  0fi  7192  findcard2  7197  findcard2s  7198  infm  7215  inffiexmid  7217  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  omct  7463  nninfisol  7479  fodjum  7492  fodju0  7493  ctssexmid  7496  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  1lt2pi  7713  nq0m0r  7829  nq0a0  7830  prarloclem5  7873  frec2uzrand  10863  frecuzrdg0  10871  frecuzrdg0t  10880  frecfzennn  10884  0tonninf  10898  1tonninf  10899  hashinfom  11239  hashunlem  11266  hash1  11274  nninfctlemfo  12842  ennnfonelemj0  13350  ennnfonelem1  13356  ennnfonelemhf1o  13362  ennnfonelemhom  13364  fnpr2o  13719  fvpr0o  13721  xpscf  13727  bj-nn0suc  17195  bj-nn0sucALT  17209  012of  17228  2o01f  17229  pwle2  17233  pwf1oexmid  17234  subctctexmid  17235  peano3nninf  17256  nninfall  17258  nninfsellemdc  17259  nninfsellemeq  17263  nninffeq  17269  nnnninfex  17271  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309