Theorem 1nn 9049

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 9040	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2272	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8073	. . . 4 |- 1 e. RR
4		elintg 3893	. . . 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 2775	. . . 4 |- z e. _V
8		eleq2 2269	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2269	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2714	. . . . 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 2917	. . 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 2564	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2176   {cab 2191   A.wral 2484   |^|cint 3885  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930   NNcn 9038

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8021

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774  df-int 3886  df-inn 9039

This theorem is referenced by:  nnind  9054  nn1suc  9057  2nn  9200  1nn0  9313  nn0p1nn  9336  1z  9400  neg1z  9406  elz2  9446  nneoor  9477  9p1e10  9508  indstr  9716  elnn1uz2  9730  zq  9749  qreccl  9765  fz01or  10235  exp3vallem  10687  exp1  10692  nnexpcl  10699  expnbnd  10810  3dec  10861  fac1  10876  faccl  10882  faclbnd3  10890  fiubnn  10977  lsw0  11043  resqrexlemf1  11352  resqrexlemcalc3  11360  resqrexlemnmsq  11361  resqrexlemnm  11362  resqrexlemcvg  11363  resqrexlemglsq  11366  resqrexlemga  11367  sumsnf  11753  cvgratnnlemnexp  11868  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  prodsnf  11936  fprodnncl  11954  eftlub  12034  eirraplem  12121  n2dvds1  12256  ndvdsp1  12276  5ndvds6  12279  gcd1  12341  bezoutr1  12387  ncoprmgcdne1b  12444  1nprm  12469  1idssfct  12470  isprm2lem  12471  qden1elz  12560  phicl2  12569  phi1  12574  phiprm  12578  eulerthlema  12585  pcpre1  12648  pczpre  12653  pcmptcl  12698  pcmpt  12699  infpnlem2  12716  mul4sq  12750  exmidunben  12830  nninfdc  12857  base0  12915  baseval  12918  baseid  12919  basendx  12920  basendxnn  12921  1strstrg  12981  2strstrg  12984  basendxnplusgndx  12990  basendxnmulrndx  12999  rngstrg  13000  lmodstrd  13029  topgrpstrd  13061  ocndx  13076  ocid  13077  basendxnocndx  13078  plendxnocndx  13079  basendxltdsndx  13084  dsndxnplusgndx  13086  dsndxnmulrndx  13087  slotsdnscsi  13088  dsndxntsetndx  13089  slotsdifdsndx  13090  basendxltunifndx  13094  unifndxntsetndx  13096  slotsdifunifndx  13097  mulg1  13498  mulg2  13500  mulgnndir  13520  setsmsdsg  14985  perfectlem1  15504  perfectlem2  15505  lgsdir2lem1  15538  lgsdir2lem4  15541  lgsdir2lem5  15542  lgsdir  15545  lgsne0  15548  lgs1  15554  lgsquad2lem2  15592  basendxltedgfndx  15642  trilpolemgt1  16015