Theorem 1nn 9132

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 9123	. . . 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 8156	. . . 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 6007   RRcr 8009   1c1 8011   + caddc 8013   NNcn 9121

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 8104

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 9122

This theorem is referenced by:  nnind  9137  nn1suc  9140  2nn  9283  1nn0  9396  nn0p1nn  9419  1z  9483  neg1z  9489  elz2  9529  nneoor  9560  9p1e10  9591  indstr  9800  elnn1uz2  9814  zq  9833  qreccl  9849  fz01or  10319  exp3vallem  10774  exp1  10779  nnexpcl  10786  expnbnd  10897  3dec  10948  fac1  10963  faccl  10969  faclbnd3  10977  fiubnn  11065  lsw0  11132  cats1un  11269  cats1fvn  11312  cats1fvnd  11313  resqrexlemf1  11535  resqrexlemcalc3  11543  resqrexlemnmsq  11544  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemglsq  11549  resqrexlemga  11550  sumsnf  11936  cvgratnnlemnexp  12051  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  prodsnf  12119  fprodnncl  12137  eftlub  12217  eirraplem  12304  n2dvds1  12439  ndvdsp1  12459  5ndvds6  12462  gcd1  12524  bezoutr1  12570  ncoprmgcdne1b  12627  1nprm  12652  1idssfct  12653  isprm2lem  12654  qden1elz  12743  phicl2  12752  phi1  12757  phiprm  12761  eulerthlema  12768  pcpre1  12831  pczpre  12836  pcmptcl  12881  pcmpt  12882  infpnlem2  12899  mul4sq  12933  exmidunben  13013  nninfdc  13040  base0  13098  baseval  13101  baseid  13102  basendx  13103  basendxnn  13104  1strstrg  13165  2strstrg  13168  basendxnplusgndx  13174  basendxnmulrndx  13183  rngstrg  13184  lmodstrd  13213  topgrpstrd  13245  ocndx  13260  ocid  13261  basendxnocndx  13262  plendxnocndx  13263  basendxltdsndx  13268  dsndxnplusgndx  13270  dsndxnmulrndx  13271  slotsdnscsi  13272  dsndxntsetndx  13273  slotsdifdsndx  13274  basendxltunifndx  13278  unifndxntsetndx  13280  slotsdifunifndx  13281  mulg1  13682  mulg2  13684  mulgnndir  13704  setsmsdsg  15170  perfectlem1  15689  perfectlem2  15690  lgsdir2lem1  15723  lgsdir2lem4  15726  lgsdir2lem5  15727  lgsdir  15730  lgsne0  15733  lgs1  15739  lgsquad2lem2  15777  basendxltedgfndx  15827  clwwlkn1  16160  trilpolemgt1  16495