Theorem 1nn 9317

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 9308	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2305	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8325	. . . 4 |- 1 e. RR
4		elintg 3978	. . . 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 2824	. . . 4 |- z e. _V
8		eleq2 2302	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2302	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2761	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 477	. . . 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 2970	. . 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 2608	1 |- 1 e. NN

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   e. wcel 2209   {cab 2224   A.wral 2528   |^|cint 3970  (class class class)co 6085   RRcr 8178   1c1 8180   + caddc 8182   NNcn 9306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8273

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-int 3971  df-inn 9307

This theorem is used by:  nnind  9322  nn1suc  9325  2nn  9470  1nn0  9583  nn0p1nn  9606  1z  9674  neg1z  9680  elz2  9720  nneoor  9752  9p1e10  9783  11nn  9805  indstr  10002  elnn1uz2  10016  zq  10035  qreccl  10051  fz01or  10528  exp3vallem  10990  exp1  10995  nnexpcl  11002  expnbnd  11114  3dec  11166  fac1  11181  faccl  11187  faclbnd3  11195  fiubnn  11287  lsw0  11366  cats1un  11507  cats1fvn  11550  cats1fvnd  11551  resqrexlemf1  11788  resqrexlemcalc3  11796  resqrexlemnmsq  11797  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemglsq  11802  resqrexlemga  11803  sumsnf  12192  cvgratnnlemnexp  12307  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  prodsnf  12375  fprodnncl  12393  eftlub  12473  eirraplem  12560  n2dvds1  12695  ndvdsp1  12715  5ndvds6  12718  gcd1  12780  bezoutr1  12826  ncoprmgcdne1b  12883  1nprm  12908  1idssfct  12909  isprm2lem  12910  qden1elz  13001  phicl2  13012  phi1  13017  phiprm  13021  eulerthlema  13028  pcpre1  13091  pczpre  13096  pcmptcl  13141  pcmpt  13142  infpnlem2  13159  mul4sq  13193  5prm  13243  7prm  13245  10nprm  13248  11prm  13249  13prm  13250  17prm  13251  19prm  13252  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  exmidunben  13366  nninfdc  13393  base0  13451  baseval  13454  baseid  13455  basendx  13456  basendxnn  13457  1strstrg  13519  2strstrg  13522  basendxnplusgndx  13528  basendxnmulrndx  13537  rngstrg  13538  lmodstrd  13567  topgrpstrd  13599  ocndx  13614  ocid  13615  basendxnocndx  13616  plendxnocndx  13617  basendxltdsndx  13622  dsndxnplusgndx  13624  dsndxnmulrndx  13625  slotsdnscsi  13626  dsndxntsetndx  13627  slotsdifdsndx  13628  basendxltunifndx  13632  unifndxntsetndx  13634  slotsdifunifndx  13635  mulg1  13981  mulg2  13983  mulgnndir  14003  setsmsdsg  15630  logfac  16048  log2ublog2  16143  perfectlem1  16197  perfectlem2  16198  bpos1  16208  bposlem5  16213  lgsdir2lem1  16245  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsdir  16252  lgsne0  16255  lgs1  16261  lgsquad2lem2  16299  basendxltedgfndx  16349  clwwlkn1  16757  konigsberglem1  16827  trilpolemgt1  17186