Theorem 1nn 8868

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 8859	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2233	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 7898	. . . 4 |- 1 e. RR
4		elintg 3832	. . . 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 183	. 2 |- ( 1 e. NN <-> A. z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } 1 e. z )
7		vex 2729	. . . 4 |- z e. _V
8		eleq2 2230	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2230	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2669	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 465	. . . 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 2870	. . 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 272	. 2 |- ( z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> 1 e. z )
14	6, 13	mprgbir 2524	1 |- 1 e. NN

Syntax hints:   /\ wa 103   <-> wb 104   e. wcel 2136   {cab 2151   A.wral 2444   |^|cint 3824  (class class class)co 5842   RRcr 7752   1c1 7754   + caddc 7756   NNcn 8857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7847

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728  df-int 3825  df-inn 8858

This theorem is referenced by:  nnind  8873  nn1suc  8876  2nn  9018  1nn0  9130  nn0p1nn  9153  1z  9217  neg1z  9223  elz2  9262  nneoor  9293  9p1e10  9324  indstr  9531  elnn1uz2  9545  zq  9564  qreccl  9580  fz01or  10046  exp3vallem  10456  exp1  10461  nnexpcl  10468  expnbnd  10578  3dec  10627  fac1  10642  faccl  10648  faclbnd3  10656  fiubnn  10743  resqrexlemf1  10950  resqrexlemcalc3  10958  resqrexlemnmsq  10959  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemglsq  10964  resqrexlemga  10965  sumsnf  11350  cvgratnnlemnexp  11465  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratnn  11472  prodsnf  11533  fprodnncl  11551  eftlub  11631  eirraplem  11717  n2dvds1  11849  ndvdsp1  11869  gcd1  11920  bezoutr1  11966  ncoprmgcdne1b  12021  1nprm  12046  1idssfct  12047  isprm2lem  12048  qden1elz  12137  phicl2  12146  phi1  12151  phiprm  12155  eulerthlema  12162  pcpre1  12224  pczpre  12229  pcmptcl  12272  pcmpt  12273  infpnlem2  12290  mul4sq  12324  exmidunben  12359  nninfdc  12386  base0  12443  baseval  12446  baseid  12447  basendx  12448  basendxnn  12449  1strstrg  12493  2strstrg  12495  basendxnplusgndx  12501  basendxnmulrndx  12509  rngstrg  12510  lmodstrd  12528  topgrpstrd  12546  setsmsdsg  13120  lgsdir2lem1  13569  lgsdir2lem4  13572  lgsdir2lem5  13573  lgsdir  13576  lgsne0  13579  lgs1  13585  trilpolemgt1  13918