Theorem 1nn 8889

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 8880	. . . 4 |- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
2	1	eleq2i 2237	. . 3 |- ( 1 e. NN <-> 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
3		1re 7919	. . . 4 |- 1 e. RR
4		elintg 3839	. . . 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 2733	. . . 4 |- z e. _V
8		eleq2 2234	. . . . 5 |- ( x = z -> ( 1 e. x <-> 1 e. z ) )
9		eleq2 2234	. . . . . 6 |- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) )
10	9	raleqbi1dv 2673	. . . . 5 |- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) )
11	8, 10	anbi12d 470	. . . 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 2874	. . 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 2528	1 |- 1 e. NN

Syntax hints:   /\ wa 103   <-> wb 104   e. wcel 2141   {cab 2156   A.wral 2448   |^|cint 3831  (class class class)co 5853   RRcr 7773   1c1 7775   + caddc 7777   NNcn 8878

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-int 3832  df-inn 8879

This theorem is referenced by:  nnind  8894  nn1suc  8897  2nn  9039  1nn0  9151  nn0p1nn  9174  1z  9238  neg1z  9244  elz2  9283  nneoor  9314  9p1e10  9345  indstr  9552  elnn1uz2  9566  zq  9585  qreccl  9601  fz01or  10067  exp3vallem  10477  exp1  10482  nnexpcl  10489  expnbnd  10599  3dec  10648  fac1  10663  faccl  10669  faclbnd3  10677  fiubnn  10765  resqrexlemf1  10972  resqrexlemcalc3  10980  resqrexlemnmsq  10981  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  sumsnf  11372  cvgratnnlemnexp  11487  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  prodsnf  11555  fprodnncl  11573  eftlub  11653  eirraplem  11739  n2dvds1  11871  ndvdsp1  11891  gcd1  11942  bezoutr1  11988  ncoprmgcdne1b  12043  1nprm  12068  1idssfct  12069  isprm2lem  12070  qden1elz  12159  phicl2  12168  phi1  12173  phiprm  12177  eulerthlema  12184  pcpre1  12246  pczpre  12251  pcmptcl  12294  pcmpt  12295  infpnlem2  12312  mul4sq  12346  exmidunben  12381  nninfdc  12408  base0  12465  baseval  12468  baseid  12469  basendx  12470  basendxnn  12471  1strstrg  12516  2strstrg  12518  basendxnplusgndx  12524  basendxnmulrndx  12532  rngstrg  12533  lmodstrd  12551  topgrpstrd  12569  setsmsdsg  13274  lgsdir2lem1  13723  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsdir  13730  lgsne0  13733  lgs1  13739  trilpolemgt1  14071