Theorem 1nn 9001

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 8992	. . . 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 8025	. . . 4 |- 1 e. RR
4		elintg 3882	. . . 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 3874  (class class class)co 5922   RRcr 7878   1c1 7880   + caddc 7882   NNcn 8990

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 7973

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 3875  df-inn 8991

This theorem is referenced by:  nnind  9006  nn1suc  9009  2nn  9152  1nn0  9265  nn0p1nn  9288  1z  9352  neg1z  9358  elz2  9397  nneoor  9428  9p1e10  9459  indstr  9667  elnn1uz2  9681  zq  9700  qreccl  9716  fz01or  10186  exp3vallem  10632  exp1  10637  nnexpcl  10644  expnbnd  10755  3dec  10806  fac1  10821  faccl  10827  faclbnd3  10835  fiubnn  10922  resqrexlemf1  11173  resqrexlemcalc3  11181  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemglsq  11187  resqrexlemga  11188  sumsnf  11574  cvgratnnlemnexp  11689  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  prodsnf  11757  fprodnncl  11775  eftlub  11855  eirraplem  11942  n2dvds1  12077  ndvdsp1  12097  5ndvds6  12100  gcd1  12154  bezoutr1  12200  ncoprmgcdne1b  12257  1nprm  12282  1idssfct  12283  isprm2lem  12284  qden1elz  12373  phicl2  12382  phi1  12387  phiprm  12391  eulerthlema  12398  pcpre1  12461  pczpre  12466  pcmptcl  12511  pcmpt  12512  infpnlem2  12529  mul4sq  12563  exmidunben  12643  nninfdc  12670  base0  12728  baseval  12731  baseid  12732  basendx  12733  basendxnn  12734  1strstrg  12794  2strstrg  12796  basendxnplusgndx  12802  basendxnmulrndx  12811  rngstrg  12812  lmodstrd  12841  topgrpstrd  12873  basendxltdsndx  12892  dsndxnplusgndx  12894  dsndxnmulrndx  12895  slotsdnscsi  12896  dsndxntsetndx  12897  slotsdifdsndx  12898  basendxltunifndx  12902  unifndxntsetndx  12904  slotsdifunifndx  12905  mulg1  13259  mulg2  13261  mulgnndir  13281  setsmsdsg  14716  perfectlem1  15235  perfectlem2  15236  lgsdir2lem1  15269  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsdir  15276  lgsne0  15279  lgs1  15285  lgsquad2lem2  15323  trilpolemgt1  15683