Theorem 1nn 9213

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 9204	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2298	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 8238	. . . 4 |- 1 e. RR
4		elintg 3941	. . . 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 2806	. . . 4 |- z e. _V
8		eleq2 2295	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2295	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2743	. . . . 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 2951	. . 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 2591	1 |- 1 e. NN

Syntax hints:   /\ wa 104   <-> wb 105   e. wcel 2202   {cab 2217   A.wral 2511   |^|cint 3933  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095   NNcn 9202

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 2213  ax-1re 8186

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-int 3934  df-inn 9203

This theorem is referenced by:  nnind  9218  nn1suc  9221  2nn  9364  1nn0  9477  nn0p1nn  9500  1z  9566  neg1z  9572  elz2  9612  nneoor  9643  9p1e10  9674  indstr  9888  elnn1uz2  9902  zq  9921  qreccl  9937  fz01or  10408  exp3vallem  10865  exp1  10870  nnexpcl  10877  expnbnd  10988  3dec  11039  fac1  11054  faccl  11060  faclbnd3  11068  fiubnn  11157  lsw0  11227  cats1un  11368  cats1fvn  11411  cats1fvnd  11412  resqrexlemf1  11648  resqrexlemcalc3  11656  resqrexlemnmsq  11657  resqrexlemnm  11658  resqrexlemcvg  11659  resqrexlemglsq  11662  resqrexlemga  11663  sumsnf  12050  cvgratnnlemnexp  12165  cvgratnnlemfm  12170  cvgratnnlemrate  12171  cvgratnn  12172  prodsnf  12233  fprodnncl  12251  eftlub  12331  eirraplem  12418  n2dvds1  12553  ndvdsp1  12573  5ndvds6  12576  gcd1  12638  bezoutr1  12684  ncoprmgcdne1b  12741  1nprm  12766  1idssfct  12767  isprm2lem  12768  qden1elz  12857  phicl2  12866  phi1  12871  phiprm  12875  eulerthlema  12882  pcpre1  12945  pczpre  12950  pcmptcl  12995  pcmpt  12996  infpnlem2  13013  mul4sq  13047  exmidunben  13127  nninfdc  13154  base0  13212  baseval  13215  baseid  13216  basendx  13217  basendxnn  13218  1strstrg  13279  2strstrg  13282  basendxnplusgndx  13288  basendxnmulrndx  13297  rngstrg  13298  lmodstrd  13327  topgrpstrd  13359  ocndx  13374  ocid  13375  basendxnocndx  13376  plendxnocndx  13377  basendxltdsndx  13382  dsndxnplusgndx  13384  dsndxnmulrndx  13385  slotsdnscsi  13386  dsndxntsetndx  13387  slotsdifdsndx  13388  basendxltunifndx  13392  unifndxntsetndx  13394  slotsdifunifndx  13395  mulg1  13796  mulg2  13798  mulgnndir  13818  setsmsdsg  15291  perfectlem1  15813  perfectlem2  15814  lgsdir2lem1  15847  lgsdir2lem4  15850  lgsdir2lem5  15851  lgsdir  15854  lgsne0  15857  lgs1  15863  lgsquad2lem2  15901  basendxltedgfndx  15951  clwwlkn1  16359  konigsberglem1  16429  trilpolemgt1  16771