Theorem uzid 11092

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 10864	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 10115	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 551	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 11082	. 2 |- ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5	3, 4	mpbird 232	1 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767   class class class wbr 4447   ` cfv 5586   <_ cle 9625   ZZcz 10860   ZZ>=cuz 11078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-pre-lttri 9562

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-neg 9804  df-z 10861  df-uz 11079

This theorem is referenced by:  uzn0  11093  uz11  11100  uzinfmi  11157  uzsupss  11170  eluzfz1  11689  eluzfz2  11690  elfz3  11692  elfz1end  11711  fzssp1  11722  fzpred  11724  fzp1ss  11727  fzpr  11731  fztp  11732  fzolb  11798  zpnn0elfzo  11852  fzosplitsnm1  11854  fzofzp1  11873  fzosplitsn  11882  fzostep1  11886  om2uzuzi  12023  axdc4uzlem  12055  seqf  12091  seqfveq  12094  seq1p  12104  faclbnd3  12332  bcm1k  12355  bcn2  12359  seqcoll  12472  ccatass  12564  swrds1  12633  swrdccat1  12639  swrdccat2  12640  splfv1  12688  splval2  12690  revccat  12697  rexuz3  13137  r19.2uz  13140  cau3lem  13143  caubnd2  13146  climconst  13322  climuni  13331  isercoll2  13447  climsup  13448  climcau  13449  serf0  13459  iseralt  13463  fsumcvg3  13507  fsumparts  13576  o1fsum  13583  abscvgcvg  13589  isum1p  13609  isumrpcl  13611  isumsup2  13614  climcndslem1  13617  climcndslem2  13618  climcnds  13619  cvgrat  13648  mertenslem1  13649  eftlub  13698  rpnnen2lem11  13812  bitsfzo  13937  bitsinv1  13944  smupval  13990  seq1st  14052  algr0  14053  eucalg  14068  oddprm  14191  pcfac  14270  pcbc  14271  vdwlem6  14356  prmlem0  14442  gsumprval  15824  gsumccat  15829  efginvrel2  16538  efgsres  16549  telgsumfzs  16806  lmconst  19525  lmmo  19644  zfbas  20129  uzrest  20130  iscau2  21448  iscau4  21450  caun0  21452  caussi  21468  equivcau  21471  lmcau  21483  mbfsup  21803  mbfinf  21804  mbflimsup  21805  plyco0  22321  dvply2g  22412  geolim3  22466  aaliou3lem2  22470  aaliou3lem3  22471  ulm2  22511  ulm0  22517  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmcn  22525  ulmdvlem3  22528  ulmdv  22529  abelthlem7  22564  ppinprm  23151  chtnprm  23153  ppiublem1  23202  chtublem  23211  chtub  23212  bposlem6  23289  lgsqr  23346  lgseisenlem4  23352  lgsquadlem1  23354  lgsquad2  23360  pntpbnd1  23496  pntlemf  23515  ostth2lem2  23544  istrkg2ld  23583  axlowdimlem17  23934  3v3e3cycl1  24317  clwwlkvbij  24474  numclwlk2lem2f  24777  esumcvg  27729  dya2ub  27878  dya2icoseg  27885  sseqmw  27967  sseqf  27968  ballotlemfp1  28067  signstfvp  28165  ntrivcvgn0  28606  fprodabs  28677  fprodefsum  28678  iprodefisumlem  28697  binomfallfaclem2  28736  mblfinlem2  29627  sdclem1  29837  fdc  29839  seqpo  29841  incsequz2  29843  geomcau  29853  bfplem2  29920  eq0rabdioph  30312  rexrabdioph  30329  jm3.1lem1  30563  fmul01lt1lem1  31134  climinf  31148  climsuse  31150  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblspltprt  31291  stoweidlem7  31307  wallispilem1  31365  wallispilem4  31368  dirkertrigeqlem1  31398