MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uzid Unicode version

Theorem uzid 11014
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
uzid

Proof of Theorem uzid
StepHypRef Expression
1 zre 10788 . . . 4
21leidd 10043 . . 3
32ancli 551 . 2
4 eluz1 11004 . 2
53, 4mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1758   class class class wbr 4409  `cfv 5537   cle 9556   cz 10784   cuz 11000
This theorem is referenced by:  uzn0  11015  uz11  11022  uzinfmi  11073  uzsupss  11086  eluzfz1  11603  eluzfz2  11604  elfz3  11606  elfz1end  11624  fzssp1  11646  fzpred  11648  fzp1ss  11651  fzpr  11656  fztp  11657  fzolb  11703  fzosplitsnm1  11753  fzofzp1  11769  fzosplitsn  11778  fzostep1  11780  om2uzuzi  11917  axdc4uzlem  11949  seqf  11984  seqfveq  11987  seq1p  11997  faclbnd3  12225  bcm1k  12248  bcn2  12252  seqcoll  12374  ccatass  12444  swrds1  12503  swrdccat1  12509  swrdccat2  12510  splfv1  12555  splval2  12557  revccat  12564  rexuz3  12994  r19.2uz  12997  cau3lem  13000  caubnd2  13003  climconst  13179  climuni  13188  isercoll2  13304  climsup  13305  climcau  13306  serf0  13316  iseralt  13320  fsumcvg3  13364  fsumparts  13427  o1fsum  13434  abscvgcvg  13440  isum1p  13462  isumrpcl  13464  isumsup2  13467  climcndslem1  13470  climcndslem2  13471  climcnds  13472  cvgrat  13501  mertenslem1  13502  eftlub  13551  rpnnen2lem11  13665  bitsfzo  13789  bitsinv1  13796  smupval  13842  seq1st  13904  algr0  13905  eucalg  13920  oddprm  14040  pcfac  14119  pcbc  14120  vdwlem6  14205  prmlem0  14291  gsumprval  15673  gsumccat  15678  efginvrel2  16385  efgsres  16396  lmconst  19264  lmmo  19383  zfbas  19868  uzrest  19869  iscau2  21187  iscau4  21189  caun0  21191  caussi  21207  equivcau  21210  lmcau  21222  mbfsup  21542  mbfinf  21543  mbflimsup  21544  plyco0  22060  dvply2g  22151  geolim3  22205  aaliou3lem2  22209  aaliou3lem3  22210  ulm2  22250  ulm0  22256  ulmcaulem  22259  ulmcau  22260  ulmss  22262  ulmcn  22264  ulmdvlem3  22267  ulmdv  22268  abelthlem7  22303  ppinprm  22890  chtnprm  22892  ppiublem1  22941  chtublem  22950  chtub  22951  bposlem6  23028  lgsqr  23085  lgseisenlem4  23091  lgsquadlem1  23093  lgsquad2  23099  pntpbnd1  23235  pntlemf  23254  ostth2lem2  23283  istrkg2ld  23322  axlowdimlem17  23673  3v3e3cycl1  23999  esumcvg  26992  dya2ub  27141  dya2icoseg  27148  sseqmw  27230  sseqf  27231  ballotlemfp1  27330  signstfvp  27428  ntrivcvgn0  27869  fprodabs  27940  fprodefsum  27941  iprodefisumlem  27960  binomfallfaclem2  27999  mblfinlem2  28889  sdclem1  29099  fdc  29101  seqpo  29103  incsequz2  29105  geomcau  29115  bfplem2  29182  eq0rabdioph  29575  rexrabdioph  29592  jm3.1lem1  29826  fmul01lt1lem1  30363  climinf  30377  climsuse  30379  ioodvbdlimc1lem2  30491  ioodvbdlimc2lem  30493  iblspltprt  30520  stoweidlem7  30536  wallispilem1  30594  wallispilem4  30597  dirkertrigeqlem1  30627  zpnn0elfzo  31098  clwwlkvbij  31340  numclwlk2lem2f  31573  telescfzgsum  31666
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 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505  ax-cnex 9475  ax-resscn 9476  ax-pre-lttri 9493
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 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6225  df-er 7235  df-en 7445  df-dom 7446  df-sdom 7447  df-pnf 9557  df-mnf 9558  df-xr 9559  df-ltxr 9560  df-le 9561  df-neg 9735  df-z 10785  df-uz 11001
  Copyright terms: Public domain W3C validator