Theorem 1nn 8901

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 8892	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2242	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 7931	. . . 4 |- 1 e. RR
4		elintg 3848	. . . 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 2738	. . . 4 |- z e. _V
8		eleq2 2239	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2239	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2678	. . . . 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 2879	. . 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 2533	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2146   {cab 2161   A.wral 2453   |^|cint 3840  (class class class)co 5865   RRcr 7785   1c1 7787   + caddc 7789   NNcn 8890

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-1re 7880

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737  df-int 3841  df-inn 8891

This theorem is referenced by:  nnind  8906  nn1suc  8909  2nn  9051  1nn0  9163  nn0p1nn  9186  1z  9250  neg1z  9256  elz2  9295  nneoor  9326  9p1e10  9357  indstr  9564  elnn1uz2  9578  zq  9597  qreccl  9613  fz01or  10079  exp3vallem  10489  exp1  10494  nnexpcl  10501  expnbnd  10611  3dec  10660  fac1  10675  faccl  10681  faclbnd3  10689  fiubnn  10776  resqrexlemf1  10983  resqrexlemcalc3  10991  resqrexlemnmsq  10992  resqrexlemnm  10993  resqrexlemcvg  10994  resqrexlemglsq  10997  resqrexlemga  10998  sumsnf  11383  cvgratnnlemnexp  11498  cvgratnnlemfm  11503  cvgratnnlemrate  11504  cvgratnn  11505  prodsnf  11566  fprodnncl  11584  eftlub  11664  eirraplem  11750  n2dvds1  11882  ndvdsp1  11902  gcd1  11953  bezoutr1  11999  ncoprmgcdne1b  12054  1nprm  12079  1idssfct  12080  isprm2lem  12081  qden1elz  12170  phicl2  12179  phi1  12184  phiprm  12188  eulerthlema  12195  pcpre1  12257  pczpre  12262  pcmptcl  12305  pcmpt  12306  infpnlem2  12323  mul4sq  12357  exmidunben  12392  nninfdc  12419  base0  12476  baseval  12479  baseid  12480  basendx  12481  basendxnn  12482  1strstrg  12527  2strstrg  12529  basendxnplusgndx  12535  basendxnmulrndx  12543  rngstrg  12544  lmodstrd  12565  topgrpstrd  12590  basendxltdsndx  12601  dsndxnplusgndx  12603  dsndxnmulrndx  12604  slotsdnscsi  12605  dsndxntsetndx  12606  slotsdifdsndx  12607  mulg1  12849  mulg2  12851  mulgnndir  12870  setsmsdsg  13549  lgsdir2lem1  13998  lgsdir2lem4  14001  lgsdir2lem5  14002  lgsdir  14005  lgsne0  14008  lgs1  14014  trilpolemgt1  14346