Theorem 1nn 9248

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 9239	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2299	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8273	. . . 4 |- 1 e. RR
4		elintg 3957	. . . 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 2816	. . . 4 |- z e. _V
8		eleq2 2296	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2296	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2753	. . . . 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 2961	. . 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 2600	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2203   {cab 2218   A.wral 2520   |^|cint 3949  (class class class)co 6050   RRcr 8126   1c1 8128   + caddc 8130   NNcn 9237

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-1re 8221

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-int 3950  df-inn 9238

This theorem is referenced by:  nnind  9253  nn1suc  9256  2nn  9399  1nn0  9512  nn0p1nn  9535  1z  9603  neg1z  9609  elz2  9649  nneoor  9680  9p1e10  9711  indstr  9925  elnn1uz2  9939  zq  9958  qreccl  9974  fz01or  10445  exp3vallem  10902  exp1  10907  nnexpcl  10914  expnbnd  11025  3dec  11076  fac1  11091  faccl  11097  faclbnd3  11105  fiubnn  11197  lsw0  11272  cats1un  11413  cats1fvn  11456  cats1fvnd  11457  resqrexlemf1  11693  resqrexlemcalc3  11701  resqrexlemnmsq  11702  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemglsq  11707  resqrexlemga  11708  sumsnf  12095  cvgratnnlemnexp  12210  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratnn  12217  prodsnf  12278  fprodnncl  12296  eftlub  12376  eirraplem  12463  n2dvds1  12598  ndvdsp1  12618  5ndvds6  12621  gcd1  12683  bezoutr1  12729  ncoprmgcdne1b  12786  1nprm  12811  1idssfct  12812  isprm2lem  12813  qden1elz  12902  phicl2  12911  phi1  12916  phiprm  12920  eulerthlema  12927  pcpre1  12990  pczpre  12995  pcmptcl  13040  pcmpt  13041  infpnlem2  13058  mul4sq  13092  exmidunben  13177  nninfdc  13204  base0  13262  baseval  13265  baseid  13266  basendx  13267  basendxnn  13268  1strstrg  13329  2strstrg  13332  basendxnplusgndx  13338  basendxnmulrndx  13347  rngstrg  13348  lmodstrd  13377  topgrpstrd  13409  ocndx  13424  ocid  13425  basendxnocndx  13426  plendxnocndx  13427  basendxltdsndx  13432  dsndxnplusgndx  13434  dsndxnmulrndx  13435  slotsdnscsi  13436  dsndxntsetndx  13437  slotsdifdsndx  13438  basendxltunifndx  13442  unifndxntsetndx  13444  slotsdifunifndx  13445  mulg1  13846  mulg2  13848  mulgnndir  13868  setsmsdsg  15345  perfectlem1  15867  perfectlem2  15868  lgsdir2lem1  15901  lgsdir2lem4  15904  lgsdir2lem5  15905  lgsdir  15908  lgsne0  15911  lgs1  15917  lgsquad2lem2  15955  basendxltedgfndx  16005  clwwlkn1  16413  konigsberglem1  16483  trilpolemgt1  16823