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  9681  neg1z  9687  elz2  9727  nneoor  9759  9p1e10  9790  11nn  9812  indstr  10009  elnn1uz2  10023  zq  10042  qreccl  10058  fz01or  10535  exp3vallem  10998  exp1  11003  nnexpcl  11010  expnbnd  11122  3dec  11174  fac1  11189  faccl  11195  faclbnd3  11203  fiubnn  11295  lsw0  11374  cats1un  11515  cats1fvn  11558  cats1fvnd  11559  resqrexlemf1  11796  resqrexlemcalc3  11804  resqrexlemnmsq  11805  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemglsq  11810  resqrexlemga  11811  sumsnf  12201  cvgratnnlemnexp  12316  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  prodsnf  12384  fprodnncl  12402  eftlub  12482  eirraplem  12569  n2dvds1  12704  ndvdsp1  12724  5ndvds6  12727  gcd1  12789  bezoutr1  12835  ncoprmgcdne1b  12892  1nprm  12917  1idssfct  12918  isprm2lem  12919  qden1elz  13010  phicl2  13021  phi1  13026  phiprm  13030  eulerthlema  13037  pcpre1  13100  pczpre  13105  pcmptcl  13150  pcmpt  13151  infpnlem2  13168  mul4sq  13202  5prm  13252  7prm  13254  10nprm  13257  11prm  13258  13prm  13259  17prm  13260  19prm  13261  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  exmidunben  13375  nninfdc  13402  base0  13460  baseval  13463  baseid  13464  basendx  13465  basendxnn  13466  1strstrg  13529  2strstrg  13532  basendxnplusgndx  13538  basendxnmulrndx  13547  rngstrg  13548  lmodstrd  13577  topgrpstrd  13609  ocndx  13624  ocid  13625  basendxnocndx  13626  plendxnocndx  13627  basendxltdsndx  13632  dsndxnplusgndx  13634  dsndxnmulrndx  13635  slotsdnscsi  13636  dsndxntsetndx  13637  slotsdifdsndx  13638  basendxltunifndx  13642  unifndxntsetndx  13644  slotsdifunifndx  13645  mulg1  13991  mulg2  13993  mulgnndir  14013  setsmsdsg  15706  logfac  16126  log2ublog2  16224  efnnfsumcl  16239  efchtqdvds  16265  prmorcht  16282  perfectlem1  16299  perfectlem2  16300  bpos1  16310  bposlem5  16315  lgsdir2lem1  16352  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsdir  16359  lgsne0  16362  lgs1  16368  lgsquad2lem2  16406  basendxltedgfndx  16456  clwwlkn1  16864  konigsberglem1  16934  trilpolemgt1  17295