Theorem uzid 11180

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

Ref	Expression
uzid	|- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Proof of Theorem uzid

Step	Hyp	Ref	Expression
1		zre 10948	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 10187	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 553	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 11170	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 235	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1872   class class class wbr 4423   ` cfv 5601   <_ cle 9683   ZZcz 10944   ZZ>=cuz 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-pre-lttri 9620

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-neg 9870  df-z 10945  df-uz 11167

This theorem is referenced by:  uzn0  11181  uz11  11188  uzinfi  11245  uzinfmiOLD  11246  uzsupss  11263  eluzfz1  11813  eluzfz2  11814  elfz3  11816  elfz1end  11836  fzssp1  11848  fzpred  11851  fzp1ss  11854  fzpr  11858  fztp  11859  elfz0add  11898  fzolb  11933  zpnn0elfzo  11992  fzosplitsnm1  11994  fzofzp1  12014  fzosplitsn  12023  fzostep1  12027  om2uzuzi  12169  axdc4uzlem  12201  seqf  12240  seqfveq  12243  seq1p  12253  faclbnd3  12483  bcm1k  12506  bcn2  12510  seqcoll  12631  ccatass  12736  ccatrn  12737  swrds1  12809  swrdccat1  12815  swrdccat2  12816  splfv1  12864  splval2  12866  revccat  12873  rexuz3  13411  r19.2uz  13414  cau3lem  13417  caubnd2  13420  climconst  13606  climuni  13615  isercoll2  13731  climsup  13732  climcau  13733  serf0  13746  iseralt  13750  fsumcvg3  13794  fsumparts  13865  o1fsum  13872  abscvgcvg  13878  isum1p  13898  isumrpcl  13900  isumsup2  13903  climcndslem1  13906  climcndslem2  13907  climcnds  13908  cvgrat  13938  mertenslem1  13939  ntrivcvgn0  13953  fprodabs  14027  binomfallfaclem2  14092  fprodefsum  14148  eftlub  14162  rpnnen2lem11  14276  bitsfzo  14408  bitsinv1  14415  smupval  14461  seq1st  14529  algr0  14530  eucalg  14545  oddprm  14764  pcfac  14843  pcbc  14844  vdwlem6  14935  prmlem0  15076  gsumprval  16523  gsumccat  16624  efginvrel2  17376  efgsres  17387  telgsumfzs  17618  lmconst  20275  lmmo  20394  zfbas  20909  uzrest  20910  iscau2  22245  iscau4  22247  caun0  22249  caussi  22265  equivcau  22268  lmcau  22280  mbfsup  22618  mbfinf  22619  mbfinfOLD  22620  mbflimsup  22621  mbflimsupOLD  22622  plyco0  23144  dvply2g  23236  geolim3  23293  aaliou3lem2  23297  aaliou3lem3  23298  ulm2  23338  ulm0  23344  ulmcaulem  23347  ulmcau  23348  ulmss  23350  ulmcn  23352  ulmdvlem3  23355  ulmdv  23356  abelthlem7  23391  ppinprm  24077  chtnprm  24079  ppiublem1  24128  chtublem  24137  chtub  24138  bposlem6  24215  lgsqr  24272  lgseisenlem4  24278  lgsquadlem1  24280  lgsquad2  24286  pntpbnd1  24422  pntlemf  24441  ostth2lem2  24470  istrkg2ld  24506  axlowdimlem17  24986  3v3e3cycl1  25370  clwwlkvbij  25527  numclwlk2lem2f  25829  fzdif2  28375  esumcvg  28915  dya2ub  29100  dya2icoseg  29107  sseqmw  29232  sseqf  29233  ballotlemfp1  29332  signstfvp  29468  iprodefisumlem  30383  poimirlem1  31905  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem9  31913  poimirlem13  31917  poimirlem14  31918  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem26  31930  poimirlem27  31931  poimirlem31  31935  poimirlem32  31936  mblfinlem2  31942  sdclem1  32036  fdc  32038  seqpo  32040  incsequz2  32042  geomcau  32052  bfplem2  32119  eq0rabdioph  35588  rexrabdioph  35606  jm3.1lem1  35842  dvgrat  36631  uzfissfz  37503  fmul01lt1lem1  37602  climinf  37624  climinfOLD  37625  climsuse  37627  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  iblspltprt  37790  stoweidlem7  37807  wallispilem1  37867  wallispilem4  37870  dirkertrigeqlem1  37900  sge0isum  38177  carageniuncllem1  38250  caratheodorylem1  38255  iccpartres  38602  iccelpart  38617  pfxccat1  38821  pfxccatpfx2  38839  fldivexpfllog2  39998  nnlog2ge0lt1  39999  logbpw2m1  40000  fllog2  40001  blennnelnn  40009  blenpw2  40011  blennnt2  40022  nnolog2flm1  40023  dig2nn0ld  40037  dig2nn1st  40038  0dig2pr01  40043  aacllem  40162