Theorem 1nn 9154

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 9145	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2298	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8178	. . . 4 |- 1 e. RR
4		elintg 3936	. . . 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 2805	. . . 4 |- z e. _V
8		eleq2 2295	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2295	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2742	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 473	. . . 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 2950	. . 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 2590	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2202   {cab 2217   A.wral 2510   |^|cint 3928  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035   NNcn 9143

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-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-int 3929  df-inn 9144

This theorem is referenced by:  nnind  9159  nn1suc  9162  2nn  9305  1nn0  9418  nn0p1nn  9441  1z  9505  neg1z  9511  elz2  9551  nneoor  9582  9p1e10  9613  indstr  9827  elnn1uz2  9841  zq  9860  qreccl  9876  fz01or  10346  exp3vallem  10803  exp1  10808  nnexpcl  10815  expnbnd  10926  3dec  10977  fac1  10992  faccl  10998  faclbnd3  11006  fiubnn  11095  lsw0  11162  cats1un  11303  cats1fvn  11346  cats1fvnd  11347  resqrexlemf1  11570  resqrexlemcalc3  11578  resqrexlemnmsq  11579  resqrexlemnm  11580  resqrexlemcvg  11581  resqrexlemglsq  11584  resqrexlemga  11585  sumsnf  11972  cvgratnnlemnexp  12087  cvgratnnlemfm  12092  cvgratnnlemrate  12093  cvgratnn  12094  prodsnf  12155  fprodnncl  12173  eftlub  12253  eirraplem  12340  n2dvds1  12475  ndvdsp1  12495  5ndvds6  12498  gcd1  12560  bezoutr1  12606  ncoprmgcdne1b  12663  1nprm  12688  1idssfct  12689  isprm2lem  12690  qden1elz  12779  phicl2  12788  phi1  12793  phiprm  12797  eulerthlema  12804  pcpre1  12867  pczpre  12872  pcmptcl  12917  pcmpt  12918  infpnlem2  12935  mul4sq  12969  exmidunben  13049  nninfdc  13076  base0  13134  baseval  13137  baseid  13138  basendx  13139  basendxnn  13140  1strstrg  13201  2strstrg  13204  basendxnplusgndx  13210  basendxnmulrndx  13219  rngstrg  13220  lmodstrd  13249  topgrpstrd  13281  ocndx  13296  ocid  13297  basendxnocndx  13298  plendxnocndx  13299  basendxltdsndx  13304  dsndxnplusgndx  13306  dsndxnmulrndx  13307  slotsdnscsi  13308  dsndxntsetndx  13309  slotsdifdsndx  13310  basendxltunifndx  13314  unifndxntsetndx  13316  slotsdifunifndx  13317  mulg1  13718  mulg2  13720  mulgnndir  13740  setsmsdsg  15207  perfectlem1  15726  perfectlem2  15727  lgsdir2lem1  15760  lgsdir2lem4  15763  lgsdir2lem5  15764  lgsdir  15767  lgsne0  15770  lgs1  15776  lgsquad2lem2  15814  basendxltedgfndx  15864  clwwlkn1  16272  trilpolemgt1  16664