Theorem 1nn 8995

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 8986	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2260	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8020	. . . 4 |- 1 e. RR
4		elintg 3879	. . . 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 2763	. . . 4 |- z e. _V
8		eleq2 2257	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2257	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2702	. . . . 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 2905	. . 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 2552	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2164   {cab 2179   A.wral 2472   |^|cint 3871  (class class class)co 5919   RRcr 7873   1c1 7875   + caddc 7877   NNcn 8984

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7968

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-int 3872  df-inn 8985

This theorem is referenced by:  nnind  9000  nn1suc  9003  2nn  9146  1nn0  9259  nn0p1nn  9282  1z  9346  neg1z  9352  elz2  9391  nneoor  9422  9p1e10  9453  indstr  9661  elnn1uz2  9675  zq  9694  qreccl  9710  fz01or  10180  exp3vallem  10614  exp1  10619  nnexpcl  10626  expnbnd  10737  3dec  10788  fac1  10803  faccl  10809  faclbnd3  10817  fiubnn  10904  resqrexlemf1  11155  resqrexlemcalc3  11163  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  sumsnf  11555  cvgratnnlemnexp  11670  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  prodsnf  11738  fprodnncl  11756  eftlub  11836  eirraplem  11923  n2dvds1  12056  ndvdsp1  12076  gcd1  12127  bezoutr1  12173  ncoprmgcdne1b  12230  1nprm  12255  1idssfct  12256  isprm2lem  12257  qden1elz  12346  phicl2  12355  phi1  12360  phiprm  12364  eulerthlema  12371  pcpre1  12433  pczpre  12438  pcmptcl  12483  pcmpt  12484  infpnlem2  12501  mul4sq  12535  exmidunben  12586  nninfdc  12613  base0  12671  baseval  12674  baseid  12675  basendx  12676  basendxnn  12677  1strstrg  12737  2strstrg  12739  basendxnplusgndx  12745  basendxnmulrndx  12754  rngstrg  12755  lmodstrd  12784  topgrpstrd  12816  basendxltdsndx  12835  dsndxnplusgndx  12837  dsndxnmulrndx  12838  slotsdnscsi  12839  dsndxntsetndx  12840  slotsdifdsndx  12841  basendxltunifndx  12845  unifndxntsetndx  12847  slotsdifunifndx  12848  mulg1  13202  mulg2  13204  mulgnndir  13224  setsmsdsg  14659  lgsdir2lem1  15185  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsdir  15192  lgsne0  15195  lgs1  15201  lgsquad2lem2  15239  trilpolemgt1  15599