Theorem 1nn 9047

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 9038	. . . 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 8071	. . . 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 5944   RRcr 7924   1c1 7926   + caddc 7928   NNcn 9036

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 8019

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 9037

This theorem is referenced by:  nnind  9052  nn1suc  9055  2nn  9198  1nn0  9311  nn0p1nn  9334  1z  9398  neg1z  9404  elz2  9444  nneoor  9475  9p1e10  9506  indstr  9714  elnn1uz2  9728  zq  9747  qreccl  9763  fz01or  10233  exp3vallem  10685  exp1  10690  nnexpcl  10697  expnbnd  10808  3dec  10859  fac1  10874  faccl  10880  faclbnd3  10888  fiubnn  10975  lsw0  11041  resqrexlemf1  11319  resqrexlemcalc3  11327  resqrexlemnmsq  11328  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemglsq  11333  resqrexlemga  11334  sumsnf  11720  cvgratnnlemnexp  11835  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  prodsnf  11903  fprodnncl  11921  eftlub  12001  eirraplem  12088  n2dvds1  12223  ndvdsp1  12243  5ndvds6  12246  gcd1  12308  bezoutr1  12354  ncoprmgcdne1b  12411  1nprm  12436  1idssfct  12437  isprm2lem  12438  qden1elz  12527  phicl2  12536  phi1  12541  phiprm  12545  eulerthlema  12552  pcpre1  12615  pczpre  12620  pcmptcl  12665  pcmpt  12666  infpnlem2  12683  mul4sq  12717  exmidunben  12797  nninfdc  12824  base0  12882  baseval  12885  baseid  12886  basendx  12887  basendxnn  12888  1strstrg  12948  2strstrg  12951  basendxnplusgndx  12957  basendxnmulrndx  12966  rngstrg  12967  lmodstrd  12996  topgrpstrd  13028  ocndx  13043  ocid  13044  basendxnocndx  13045  plendxnocndx  13046  basendxltdsndx  13051  dsndxnplusgndx  13053  dsndxnmulrndx  13054  slotsdnscsi  13055  dsndxntsetndx  13056  slotsdifdsndx  13057  basendxltunifndx  13061  unifndxntsetndx  13063  slotsdifunifndx  13064  mulg1  13465  mulg2  13467  mulgnndir  13487  setsmsdsg  14952  perfectlem1  15471  perfectlem2  15472  lgsdir2lem1  15505  lgsdir2lem4  15508  lgsdir2lem5  15509  lgsdir  15512  lgsne0  15515  lgs1  15521  lgsquad2lem2  15559  basendxltedgfndx  15609  trilpolemgt1  15978