Theorem uzid 10987

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 10762	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 10018	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 551	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 10977	. 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 1758   class class class wbr 4401   ` cfv 5527   <_ cle 9531   ZZcz 10758   ZZ>=cuz 10973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-pre-lttri 9468

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-ov 6204  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-neg 9710  df-z 10759  df-uz 10974

This theorem is referenced by:  uzn0  10988  uz11  10995  uzinfmi  11046  uzsupss  11059  eluzfz1  11576  eluzfz2  11577  elfz3  11579  elfz1end  11597  fzssp1  11619  fzpred  11621  fzp1ss  11624  fzpr  11629  fztp  11630  fzolb  11676  fzosplitsnm1  11726  fzofzp1  11742  fzosplitsn  11751  fzostep1  11753  om2uzuzi  11890  axdc4uzlem  11922  seqf  11945  seqfveq  11948  seq1p  11958  faclbnd3  12186  bcm1k  12209  bcn2  12213  seqcoll  12335  ccatass  12405  swrds1  12464  swrdccat1  12470  swrdccat2  12471  splfv1  12516  splval2  12518  revccat  12525  rexuz3  12955  r19.2uz  12958  cau3lem  12961  caubnd2  12964  climconst  13140  climuni  13149  isercoll2  13265  climsup  13266  climcau  13267  serf0  13277  iseralt  13281  fsumcvg3  13325  fsumparts  13388  o1fsum  13395  abscvgcvg  13401  isum1p  13423  isumrpcl  13425  isumsup2  13428  climcndslem1  13431  climcndslem2  13432  climcnds  13433  cvgrat  13462  mertenslem1  13463  eftlub  13512  rpnnen2lem11  13626  bitsfzo  13750  bitsinv1  13757  smupval  13803  seq1st  13865  algr0  13866  eucalg  13881  oddprm  14001  pcfac  14080  pcbc  14081  vdwlem6  14166  prmlem0  14252  gsumprval  15634  gsumccat  15639  efginvrel2  16346  efgsres  16357  lmconst  18998  lmmo  19117  zfbas  19602  uzrest  19603  iscau2  20921  iscau4  20923  caun0  20925  caussi  20941  equivcau  20944  lmcau  20956  mbfsup  21276  mbfinf  21277  mbflimsup  21278  plyco0  21794  dvply2g  21885  geolim3  21939  aaliou3lem2  21943  aaliou3lem3  21944  ulm2  21984  ulm0  21990  ulmcaulem  21993  ulmcau  21994  ulmss  21996  ulmcn  21998  ulmdvlem3  22001  ulmdv  22002  abelthlem7  22037  ppinprm  22624  chtnprm  22626  ppiublem1  22675  chtublem  22684  chtub  22685  bposlem6  22762  lgsqr  22819  lgseisenlem4  22825  lgsquadlem1  22827  lgsquad2  22833  pntpbnd1  22969  pntlemf  22988  ostth2lem2  23017  istrkg2ld  23056  axlowdimlem17  23357  3v3e3cycl1  23683  esumcvg  26681  dya2ub  26830  dya2icoseg  26837  sseqmw  26919  sseqf  26920  ballotlemfp1  27019  signstfvp  27117  ntrivcvgn0  27558  fprodabs  27629  fprodefsum  27630  iprodefisumlem  27649  binomfallfaclem2  27688  mblfinlem2  28578  sdclem1  28788  fdc  28790  seqpo  28792  incsequz2  28794  geomcau  28804  bfplem2  28871  eq0rabdioph  29264  rexrabdioph  29281  jm3.1lem1  29515  fmul01lt1lem1  29914  climinf  29928  climsuse  29930  stoweidlem7  29951  wallispilem1  30009  wallispilem4  30012  zpnn0elfzo  30370  clwwlkvbij  30612  numclwlk2lem2f  30845  telescfzgsum  30963