Theorem uzid 10867

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 10642	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 9898	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 551	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 10857	. 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 1756   class class class wbr 4287   ` cfv 5413   <_ cle 9411   ZZcz 10638   ZZ>=cuz 10853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-pre-lttri 9348

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-neg 9590  df-z 10639  df-uz 10854

This theorem is referenced by:  uzn0  10868  uz11  10875  uzinfmi  10926  uzsupss  10939  eluzfz1  11450  eluzfz2  11451  elfz3  11453  elfz1end  11471  fzssp1  11493  fzpred  11495  fzp1ss  11498  fzpr  11503  fztp  11504  fzolb  11550  fzosplitsnm1  11600  fzofzp1  11616  fzosplitsn  11625  fzostep1  11627  om2uzuzi  11764  axdc4uzlem  11796  seqf  11819  seqfveq  11822  seq1p  11832  faclbnd3  12060  bcm1k  12083  bcn2  12087  seqcoll  12208  ccatass  12278  swrds1  12337  swrdccat1  12343  swrdccat2  12344  splfv1  12389  splval2  12391  revccat  12398  rexuz3  12828  r19.2uz  12831  cau3lem  12834  caubnd2  12837  climconst  13013  climuni  13022  isercoll2  13138  climsup  13139  climcau  13140  serf0  13150  iseralt  13154  fsumcvg3  13198  fsumparts  13261  o1fsum  13268  abscvgcvg  13274  isum1p  13296  isumrpcl  13298  isumsup2  13301  climcndslem1  13304  climcndslem2  13305  climcnds  13306  cvgrat  13335  mertenslem1  13336  eftlub  13385  rpnnen2lem11  13499  bitsfzo  13623  bitsinv1  13630  smupval  13676  seq1st  13738  algr0  13739  eucalg  13754  oddprm  13874  pcfac  13953  pcbc  13954  vdwlem6  14039  prmlem0  14125  gsumprval  15505  gsumccat  15510  efginvrel2  16215  efgsres  16226  lmconst  18840  lmmo  18959  zfbas  19444  uzrest  19445  iscau2  20763  iscau4  20765  caun0  20767  caussi  20783  equivcau  20786  lmcau  20798  mbfsup  21117  mbfinf  21118  mbflimsup  21119  plyco0  21635  dvply2g  21726  geolim3  21780  aaliou3lem2  21784  aaliou3lem3  21785  ulm2  21825  ulm0  21831  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmcn  21839  ulmdvlem3  21842  ulmdv  21843  abelthlem7  21878  ppinprm  22465  chtnprm  22467  ppiublem1  22516  chtublem  22525  chtub  22526  bposlem6  22603  lgsqr  22660  lgseisenlem4  22666  lgsquadlem1  22668  lgsquad2  22674  pntpbnd1  22810  pntlemf  22829  ostth2lem2  22858  axlowdimlem17  23155  3v3e3cycl1  23481  esumcvg  26487  dya2ub  26637  dya2icoseg  26644  sseqmw  26726  sseqf  26727  ballotlemfp1  26826  signstfvp  26924  ntrivcvgn0  27364  fprodabs  27435  fprodefsum  27436  iprodefisumlem  27455  binomfallfaclem2  27494  mblfinlem2  28382  sdclem1  28592  fdc  28594  seqpo  28596  incsequz2  28598  geomcau  28608  bfplem2  28675  eq0rabdioph  29068  rexrabdioph  29085  jm3.1lem1  29319  fmul01lt1lem1  29718  climinf  29732  climsuse  29734  stoweidlem7  29755  wallispilem1  29813  wallispilem4  29816  zpnn0elfzo  30174  clwwlkvbij  30416  numclwlk2lem2f  30649