Theorem 1nn 9324

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)

Assertion

Ref	Expression
1nn	|- 1 e. NN

Proof of Theorem 1nn

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 9315	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2305	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8331	. . . 4 |- 1 e. RR
4		elintg 3978	. . . 4 |- ( 1 e. RR -> ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } 1 e. z ) )
5	3, 4	ax-mp 5	. . 3 |- ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } 1 e. z )
6	2, 5	bitri 184	. 2 |- ( 1 e. NN <-> A. z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } 1 e. z )
7		vex 2824	. . . 4 |- z e. _V
8		eleq2 2302	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2302	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2761	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 477	. . . 4 |- ( x = z -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) ) )
12	7, 11	elab 2970	. . 3 |- ( z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) )
13	12	simplbi 274	. 2 |- ( z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> 1 e. z )
14	6, 13	mprgbir 2608	1 |- 1 e. NN

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   e. wcel 2209   {cab 2224   A.wral 2528   |^|cint 3970  (class class class)co 6088   RRcr 8184   1c1 8186   + caddc 8188   NNcn 9313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  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-1re 8279

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-ral 2533  df-v 2823  df-int 3971  df-inn 9314

This theorem is used by:  nnind  9329  nn1suc  9332  2nn  9477  1nn0  9590  nn0p1nn  9613  1z  9679  neg1z  9685  elz2  9725  nneoor  9758  9p1e10  9789  11nn  9811  indstr  10008  elnn1uz2  10022  zq  10041  qreccl  10057  fz01or  10534  exp3vallem  10997  exp1  11002  nnexpcl  11009  expnbnd  11121  3dec  11173  fac1  11188  faccl  11194  faclbnd3  11202  fiubnn  11294  lsw0  11373  cats1un  11514  cats1fvn  11557  cats1fvnd  11558  resqrexlemf1  11795  resqrexlemcalc3  11803  resqrexlemnmsq  11804  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemglsq  11809  resqrexlemga  11810  sumsnf  12200  cvgratnnlemnexp  12315  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  prodsnf  12383  fprodnncl  12401  eftlub  12481  eirraplem  12568  n2dvds1  12703  ndvdsp1  12723  5ndvds6  12726  gcd1  12788  bezoutr1  12834  ncoprmgcdne1b  12891  1nprm  12916  1idssfct  12917  isprm2lem  12918  qden1elz  13009  phicl2  13020  phi1  13025  phiprm  13029  eulerthlema  13036  pcpre1  13099  pczpre  13104  pcmptcl  13149  pcmpt  13150  infpnlem2  13167  mul4sq  13201  5prm  13251  7prm  13253  10nprm  13256  11prm  13257  13prm  13258  17prm  13259  19prm  13260  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  exmidunben  13374  nninfdc  13401  base0  13459  baseval  13462  baseid  13463  basendx  13464  basendxnn  13465  1strstrg  13528  2strstrg  13531  basendxnplusgndx  13537  basendxnmulrndx  13546  rngstrg  13547  lmodstrd  13576  topgrpstrd  13608  ocndx  13623  ocid  13624  basendxnocndx  13625  plendxnocndx  13626  basendxltdsndx  13631  dsndxnplusgndx  13633  dsndxnmulrndx  13634  slotsdnscsi  13635  dsndxntsetndx  13636  slotsdifdsndx  13637  basendxltunifndx  13641  unifndxntsetndx  13643  slotsdifunifndx  13644  mulg1  13990  mulg2  13992  mulgnndir  14012  setsmsdsg  15723  logfac  16143  log2ublog2  16241  efnnfsumcl  16256  efchtqdvds  16282  prmorcht  16299  perfectlem1  16316  perfectlem2  16317  bpos1  16327  bposlem5  16332  lgsdir2lem1  16369  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsdir  16376  lgsne0  16379  lgs1  16385  lgsquad2lem2  16423  basendxltedgfndx  16473  clwwlkn1  16881  konigsberglem1  16951  trilpolemgt1  17312