Theorem 1nn 8638

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 8629	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2181	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 7686	. . . 4 |- 1 e. RR
4		elintg 3745	. . . 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 7	. . 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 2660	. . . 4 |- z e. _V
8		eleq2 2178	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2178	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2608	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 462	. . . 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 2798	. . 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 270	. 2 |- ( z e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> 1 e. z )
14	6, 13	mprgbir 2464	1 |- 1 e. NN

Syntax hints:   /\ wa 103   <-> wb 104   e. wcel 1463   {cab 2101   A.wral 2390   |^|cint 3737  (class class class)co 5728   RRcr 7543   1c1 7545   + caddc 7547   NNcn 8627

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1re 7636

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-v 2659  df-int 3738  df-inn 8628

This theorem is referenced by:  nnind  8643  nn1suc  8646  2nn  8782  1nn0  8894  nn0p1nn  8917  1z  8981  neg1z  8987  elz2  9023  nneoor  9054  9p1e10  9085  indstr  9287  elnn1uz2  9300  zq  9317  qreccl  9333  fz01or  9781  exp3vallem  10184  exp1  10189  nnexpcl  10196  expnbnd  10305  3dec  10351  fac1  10365  faccl  10371  faclbnd3  10379  resqrexlemf1  10669  resqrexlemcalc3  10677  resqrexlemnmsq  10678  resqrexlemnm  10679  resqrexlemcvg  10680  resqrexlemglsq  10683  resqrexlemga  10684  sumsnf  11067  cvgratnnlemnexp  11182  cvgratnnlemfm  11187  cvgratnnlemrate  11188  cvgratnn  11189  eftlub  11244  eirraplem  11328  n2dvds1  11454  ndvdsp1  11474  gcd1  11520  bezoutr1  11564  ncoprmgcdne1b  11613  1nprm  11638  1idssfct  11639  isprm2lem  11640  qden1elz  11725  phicl2  11732  phi1  11737  phiprm  11741  exmidunben  11781  base0  11848  baseval  11851  baseid  11852  basendx  11853  basendxnn  11854  1strstrg  11897  2strstrg  11899  basendxnplusgndx  11905  basendxnmulrndx  11913  rngstrg  11914  lmodstrd  11932  topgrpstrd  11950  setsmsdsg  12466  trilpolemgt1  12916