Theorem 1nn 9121

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 9112	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2296	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8145	. . . 4 |- 1 e. RR
4		elintg 3931	. . . 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 2802	. . . 4 |- z e. _V
8		eleq2 2293	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2293	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2740	. . . . 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 2947	. . 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 2588	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2200   {cab 2215   A.wral 2508   |^|cint 3923  (class class class)co 6001   RRcr 7998   1c1 8000   + caddc 8002   NNcn 9110

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-int 3924  df-inn 9111

This theorem is referenced by:  nnind  9126  nn1suc  9129  2nn  9272  1nn0  9385  nn0p1nn  9408  1z  9472  neg1z  9478  elz2  9518  nneoor  9549  9p1e10  9580  indstr  9788  elnn1uz2  9802  zq  9821  qreccl  9837  fz01or  10307  exp3vallem  10762  exp1  10767  nnexpcl  10774  expnbnd  10885  3dec  10936  fac1  10951  faccl  10957  faclbnd3  10965  fiubnn  11052  lsw0  11119  cats1un  11253  cats1fvn  11296  cats1fvnd  11297  resqrexlemf1  11519  resqrexlemcalc3  11527  resqrexlemnmsq  11528  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemglsq  11533  resqrexlemga  11534  sumsnf  11920  cvgratnnlemnexp  12035  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  prodsnf  12103  fprodnncl  12121  eftlub  12201  eirraplem  12288  n2dvds1  12423  ndvdsp1  12443  5ndvds6  12446  gcd1  12508  bezoutr1  12554  ncoprmgcdne1b  12611  1nprm  12636  1idssfct  12637  isprm2lem  12638  qden1elz  12727  phicl2  12736  phi1  12741  phiprm  12745  eulerthlema  12752  pcpre1  12815  pczpre  12820  pcmptcl  12865  pcmpt  12866  infpnlem2  12883  mul4sq  12917  exmidunben  12997  nninfdc  13024  base0  13082  baseval  13085  baseid  13086  basendx  13087  basendxnn  13088  1strstrg  13149  2strstrg  13152  basendxnplusgndx  13158  basendxnmulrndx  13167  rngstrg  13168  lmodstrd  13197  topgrpstrd  13229  ocndx  13244  ocid  13245  basendxnocndx  13246  plendxnocndx  13247  basendxltdsndx  13252  dsndxnplusgndx  13254  dsndxnmulrndx  13255  slotsdnscsi  13256  dsndxntsetndx  13257  slotsdifdsndx  13258  basendxltunifndx  13262  unifndxntsetndx  13264  slotsdifunifndx  13265  mulg1  13666  mulg2  13668  mulgnndir  13688  setsmsdsg  15154  perfectlem1  15673  perfectlem2  15674  lgsdir2lem1  15707  lgsdir2lem4  15710  lgsdir2lem5  15711  lgsdir  15714  lgsne0  15717  lgs1  15723  lgsquad2lem2  15761  basendxltedgfndx  15811  trilpolemgt1  16407