Theorem 1nn 9082

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 9073	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2274	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8106	. . . 4 |- 1 e. RR
4		elintg 3907	. . . 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 2779	. . . 4 |- z e. _V
8		eleq2 2271	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2271	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2717	. . . . 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 2924	. . 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 2566	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2178   {cab 2193   A.wral 2486   |^|cint 3899  (class class class)co 5967   RRcr 7959   1c1 7961   + caddc 7963   NNcn 9071

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-int 3900  df-inn 9072

This theorem is referenced by:  nnind  9087  nn1suc  9090  2nn  9233  1nn0  9346  nn0p1nn  9369  1z  9433  neg1z  9439  elz2  9479  nneoor  9510  9p1e10  9541  indstr  9749  elnn1uz2  9763  zq  9782  qreccl  9798  fz01or  10268  exp3vallem  10722  exp1  10727  nnexpcl  10734  expnbnd  10845  3dec  10896  fac1  10911  faccl  10917  faclbnd3  10925  fiubnn  11012  lsw0  11078  cats1un  11212  resqrexlemf1  11434  resqrexlemcalc3  11442  resqrexlemnmsq  11443  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemglsq  11448  resqrexlemga  11449  sumsnf  11835  cvgratnnlemnexp  11950  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  prodsnf  12018  fprodnncl  12036  eftlub  12116  eirraplem  12203  n2dvds1  12338  ndvdsp1  12358  5ndvds6  12361  gcd1  12423  bezoutr1  12469  ncoprmgcdne1b  12526  1nprm  12551  1idssfct  12552  isprm2lem  12553  qden1elz  12642  phicl2  12651  phi1  12656  phiprm  12660  eulerthlema  12667  pcpre1  12730  pczpre  12735  pcmptcl  12780  pcmpt  12781  infpnlem2  12798  mul4sq  12832  exmidunben  12912  nninfdc  12939  base0  12997  baseval  13000  baseid  13001  basendx  13002  basendxnn  13003  1strstrg  13063  2strstrg  13066  basendxnplusgndx  13072  basendxnmulrndx  13081  rngstrg  13082  lmodstrd  13111  topgrpstrd  13143  ocndx  13158  ocid  13159  basendxnocndx  13160  plendxnocndx  13161  basendxltdsndx  13166  dsndxnplusgndx  13168  dsndxnmulrndx  13169  slotsdnscsi  13170  dsndxntsetndx  13171  slotsdifdsndx  13172  basendxltunifndx  13176  unifndxntsetndx  13178  slotsdifunifndx  13179  mulg1  13580  mulg2  13582  mulgnndir  13602  setsmsdsg  15067  perfectlem1  15586  perfectlem2  15587  lgsdir2lem1  15620  lgsdir2lem4  15623  lgsdir2lem5  15624  lgsdir  15627  lgsne0  15630  lgs1  15636  lgsquad2lem2  15674  basendxltedgfndx  15724  trilpolemgt1  16180