Theorem 1nn 9018

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 9009	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2263	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8042	. . . 4 |- 1 e. RR
4		elintg 3883	. . . 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 2766	. . . 4 |- z e. _V
8		eleq2 2260	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2260	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2705	. . . . 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 2908	. . 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 2555	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2167   {cab 2182   A.wral 2475   |^|cint 3875  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899   NNcn 9007

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7990

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-int 3876  df-inn 9008

This theorem is referenced by:  nnind  9023  nn1suc  9026  2nn  9169  1nn0  9282  nn0p1nn  9305  1z  9369  neg1z  9375  elz2  9414  nneoor  9445  9p1e10  9476  indstr  9684  elnn1uz2  9698  zq  9717  qreccl  9733  fz01or  10203  exp3vallem  10649  exp1  10654  nnexpcl  10661  expnbnd  10772  3dec  10823  fac1  10838  faccl  10844  faclbnd3  10852  fiubnn  10939  resqrexlemf1  11190  resqrexlemcalc3  11198  resqrexlemnmsq  11199  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemglsq  11204  resqrexlemga  11205  sumsnf  11591  cvgratnnlemnexp  11706  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  prodsnf  11774  fprodnncl  11792  eftlub  11872  eirraplem  11959  n2dvds1  12094  ndvdsp1  12114  5ndvds6  12117  gcd1  12179  bezoutr1  12225  ncoprmgcdne1b  12282  1nprm  12307  1idssfct  12308  isprm2lem  12309  qden1elz  12398  phicl2  12407  phi1  12412  phiprm  12416  eulerthlema  12423  pcpre1  12486  pczpre  12491  pcmptcl  12536  pcmpt  12537  infpnlem2  12554  mul4sq  12588  exmidunben  12668  nninfdc  12695  base0  12753  baseval  12756  baseid  12757  basendx  12758  basendxnn  12759  1strstrg  12819  2strstrg  12821  basendxnplusgndx  12827  basendxnmulrndx  12836  rngstrg  12837  lmodstrd  12866  topgrpstrd  12898  ocndx  12913  ocid  12914  basendxnocndx  12915  plendxnocndx  12916  basendxltdsndx  12921  dsndxnplusgndx  12923  dsndxnmulrndx  12924  slotsdnscsi  12925  dsndxntsetndx  12926  slotsdifdsndx  12927  basendxltunifndx  12931  unifndxntsetndx  12933  slotsdifunifndx  12934  mulg1  13335  mulg2  13337  mulgnndir  13357  setsmsdsg  14800  perfectlem1  15319  perfectlem2  15320  lgsdir2lem1  15353  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsdir  15360  lgsne0  15363  lgs1  15369  lgsquad2lem2  15407  trilpolemgt1  15770