Theorem uzid 11057

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 10827	. . . 4 |- ( M e. ZZ -> M e. RR )
2	1	leidd 10077	. . 3 |- ( M e. ZZ -> M <_ M )
3	2	ancli 549	. 2 |- ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4		eluz1 11047	. 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 367   e. wcel 1840   class class class wbr 4392   ` cfv 5523   <_ cle 9577   ZZcz 10823   ZZ>=cuz 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-un 6528  ax-cnex 9496  ax-resscn 9497  ax-pre-lttri 9514

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 973  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-nel 2599  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-sbc 3275  df-csb 3371  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-f1 5528  df-fo 5529  df-f1o 5530  df-fv 5531  df-ov 6235  df-er 7266  df-en 7473  df-dom 7474  df-sdom 7475  df-pnf 9578  df-mnf 9579  df-xr 9580  df-ltxr 9581  df-le 9582  df-neg 9762  df-z 10824  df-uz 11044

This theorem is referenced by:  uzn0  11058  uz11  11065  uzinfmi  11122  uzsupss  11135  eluzfz1  11662  eluzfz2  11663  elfz3  11665  elfz1end  11684  fzssp1  11696  fzpred  11698  fzp1ss  11701  fzpr  11705  fztp  11706  elfz0add  11745  fzolb  11776  zpnn0elfzo  11835  fzosplitsnm1  11837  fzofzp1  11857  fzosplitsn  11866  fzostep1  11870  om2uzuzi  12012  axdc4uzlem  12044  seqf  12080  seqfveq  12083  seq1p  12093  faclbnd3  12322  bcm1k  12345  bcn2  12349  seqcoll  12466  ccatass  12564  ccatrn  12565  swrds1  12637  swrdccat1  12643  swrdccat2  12644  splfv1  12692  splval2  12694  revccat  12701  rexuz3  13235  r19.2uz  13238  cau3lem  13241  caubnd2  13244  climconst  13420  climuni  13429  isercoll2  13545  climsup  13546  climcau  13547  serf0  13557  iseralt  13561  fsumcvg3  13605  fsumparts  13676  o1fsum  13683  abscvgcvg  13689  isum1p  13709  isumrpcl  13711  isumsup2  13714  climcndslem1  13717  climcndslem2  13718  climcnds  13719  cvgrat  13749  mertenslem1  13750  ntrivcvgn0  13764  fprodabs  13835  binomfallfaclem2  13890  fprodefsum  13929  eftlub  13943  rpnnen2lem11  14057  bitsfzo  14184  bitsinv1  14191  smupval  14237  seq1st  14299  algr0  14300  eucalg  14315  oddprm  14438  pcfac  14517  pcbc  14518  vdwlem6  14603  prmlem0  14690  gsumprval  16122  gsumccat  16223  efginvrel2  16959  efgsres  16970  telgsumfzs  17228  lmconst  19945  lmmo  20064  zfbas  20579  uzrest  20580  iscau2  21898  iscau4  21900  caun0  21902  caussi  21918  equivcau  21921  lmcau  21933  mbfsup  22253  mbfinf  22254  mbflimsup  22255  plyco0  22771  dvply2g  22863  geolim3  22917  aaliou3lem2  22921  aaliou3lem3  22922  ulm2  22962  ulm0  22968  ulmcaulem  22971  ulmcau  22972  ulmss  22974  ulmcn  22976  ulmdvlem3  22979  ulmdv  22980  abelthlem7  23015  ppinprm  23697  chtnprm  23699  ppiublem1  23748  chtublem  23757  chtub  23758  bposlem6  23835  lgsqr  23892  lgseisenlem4  23898  lgsquadlem1  23900  lgsquad2  23906  pntpbnd1  24042  pntlemf  24061  ostth2lem2  24090  istrkg2ld  24129  axlowdimlem17  24560  3v3e3cycl1  24943  clwwlkvbij  25100  numclwlk2lem2f  25402  esumcvg  28414  dya2ub  28599  dya2icoseg  28606  sseqmw  28717  sseqf  28718  ballotlemfp1  28817  signstfvp  28915  iprodefisumlem  29830  mblfinlem2  31388  sdclem1  31482  fdc  31484  seqpo  31486  incsequz2  31488  geomcau  31498  bfplem2  31565  eq0rabdioph  35035  rexrabdioph  35053  jm3.1lem1  35285  dvgrat  36005  fmul01lt1lem1  36913  climinf  36947  climsuse  36949  ioodvbdlimc1lem2  37064  ioodvbdlimc2lem  37066  iblspltprt  37107  stoweidlem7  37124  wallispilem1  37182  wallispilem4  37185  dirkertrigeqlem1  37215  iccpartres  37648  iccelpart  37663  pfxccat1  37829  pfxccatpfx2  37847  fldivexpfllog2  38630  nnlog2ge0lt1  38631  logbpw2m1  38632  fllog2  38633  blennnelnn  38641  blenpw2  38643  blennnt2  38654  nnolog2flm1  38655  dig2nn0ld  38669  dig2nn1st  38670  0dig2pr01  38675  aacllem  38794