Theorem uzid 11207

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 10975	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 10213	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 558	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 11197	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 240	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   class class class wbr 4418   ` cfv 5605   <_ cle 9707   ZZcz 10971   ZZ>=cuz 11193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-pre-lttri 9644

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-neg 9894  df-z 10972  df-uz 11194

This theorem is referenced by:  uzn0  11208  uz11  11215  uzinfi  11272  uzinfmiOLD  11273  uzsupss  11290  eluzfz1  11841  eluzfz2  11842  elfz3  11844  elfz1end  11864  fzssp1  11876  fzpred  11879  fzp1ss  11882  fzpr  11886  fztp  11887  elfz0add  11926  fzolb  11963  zpnn0elfzo  12023  fzosplitsnm1  12025  fzofzp1  12045  fzosplitsn  12054  fzostep1  12058  om2uzuzi  12201  axdc4uzlem  12233  seqf  12272  seqfveq  12275  seq1p  12285  faclbnd3  12515  bcm1k  12538  bcn2  12542  seqcoll  12666  ccatass  12774  ccatrn  12775  swrds1  12850  swrdccat1  12856  swrdccat2  12857  splfv1  12905  splval2  12907  revccat  12914  rexuz3  13466  r19.2uz  13469  cau3lem  13472  caubnd2  13475  climconst  13662  climuni  13671  isercoll2  13787  climsup  13788  climcau  13789  serf0  13802  iseralt  13806  fsumcvg3  13850  fsumparts  13921  o1fsum  13928  abscvgcvg  13934  isum1p  13954  isumrpcl  13956  isumsup2  13959  climcndslem1  13962  climcndslem2  13963  climcnds  13964  cvgrat  13994  mertenslem1  13995  ntrivcvgn0  14009  fprodabs  14083  binomfallfaclem2  14148  fprodefsum  14204  eftlub  14218  rpnnen2lem11  14332  bitsfzo  14464  bitsinv1  14471  smupval  14517  seq1st  14585  algr0  14586  eucalg  14601  oddprm  14820  pcfac  14899  pcbc  14900  vdwlem6  14991  prmlem0  15132  gsumprval  16579  gsumccat  16680  efginvrel2  17432  efgsres  17443  telgsumfzs  17674  lmconst  20332  lmmo  20451  zfbas  20966  uzrest  20967  iscau2  22302  iscau4  22304  caun0  22306  caussi  22322  equivcau  22325  lmcau  22337  mbfsup  22676  mbfinf  22677  mbfinfOLD  22678  mbflimsup  22679  mbflimsupOLD  22680  plyco0  23202  dvply2g  23294  geolim3  23351  aaliou3lem2  23355  aaliou3lem3  23356  ulm2  23396  ulm0  23402  ulmcaulem  23405  ulmcau  23406  ulmss  23408  ulmcn  23410  ulmdvlem3  23413  ulmdv  23414  abelthlem7  23449  ppinprm  24135  chtnprm  24137  ppiublem1  24186  chtublem  24195  chtub  24196  bposlem6  24273  lgsqr  24330  lgseisenlem4  24336  lgsquadlem1  24338  lgsquad2  24344  pntpbnd1  24480  pntlemf  24499  ostth2lem2  24528  istrkg2ld  24564  axlowdimlem17  25044  3v3e3cycl1  25428  clwwlkvbij  25585  numclwlk2lem2f  25887  fzdif2  28421  esumcvg  28958  dya2ub  29142  dya2icoseg  29149  sseqmw  29274  sseqf  29275  ballotlemfp1  29374  signstfvp  29510  iprodefisumlem  30426  poimirlem1  31987  poimirlem2  31988  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem9  31995  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem26  32012  poimirlem27  32013  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  sdclem1  32118  fdc  32120  seqpo  32122  incsequz2  32124  geomcau  32134  bfplem2  32201  eq0rabdioph  35665  rexrabdioph  35683  jm3.1lem1  35918  dvgrat  36706  uzfissfz  37624  fmul01lt1lem1  37748  climinf  37770  climinfOLD  37771  climsuse  37773  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  iblspltprt  37936  stoweidlem7  37968  wallispilem1  38028  wallispilem4  38031  dirkertrigeqlem1  38061  sge0isum  38372  carageniuncllem1  38450  caratheodorylem1  38455  iccpartres  38867  iccelpart  38882  pfxccat1  39088  pfxccatpfx2  39106  fldivexpfllog2  40745  nnlog2ge0lt1  40746  logbpw2m1  40747  fllog2  40748  blennnelnn  40756  blenpw2  40758  blennnt2  40769  nnolog2flm1  40770  dig2nn0ld  40784  dig2nn1st  40785  0dig2pr01  40790  aacllem  40909