MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzel2 Structured version   Visualization version   GIF version

Theorem eluzel2 11677
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
eluzel2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)

Proof of Theorem eluzel2
StepHypRef Expression
1 elfvdm 6207 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ dom ℤ)
2 uzf 11675 . . 3 :ℤ⟶𝒫 ℤ
32fdmi 6039 . 2 dom ℤ = ℤ
41, 3syl6eleq 2709 1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  𝒫 cpw 4149  dom cdm 5104  cfv 5876  cz 11362  cuz 11672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-cnex 9977  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-ov 6638  df-neg 10254  df-z 11363  df-uz 11673
This theorem is referenced by:  eluz2  11678  uztrn  11689  uzneg  11691  uzss  11693  uz11  11695  eluzadd  11701  uzm1  11703  uzin  11705  uzind4  11731  uzsupss  11765  elfz5  12319  elfzel1  12326  eluzfz1  12333  fzsplit2  12351  fzopth  12363  ssfzunsn  12372  fzpred  12374  fzpreddisj  12375  uzsplit  12396  uzdisj  12397  fzm1  12404  uznfz  12407  nn0disj  12439  preduz  12445  fzolb  12460  fzoss2  12480  fzouzdisj  12488  ige2m2fzo  12514  fzen2  12751  seqp1  12799  seqcl  12804  seqfeq2  12807  seqfveq  12808  seqshft2  12810  seqsplit  12817  seqcaopr3  12819  seqf1olem2a  12822  seqf1olem1  12823  seqf1olem2  12824  seqid  12829  seqhomo  12831  seqz  12832  leexp2a  12899  hashfz  13197  fzsdom2  13198  hashfzo  13199  hashfzp1  13201  seqcoll  13231  rexanuz2  14070  cau4  14077  clim2ser  14366  clim2ser2  14367  climserle  14374  caurcvg  14388  caucvg  14390  fsumcvg  14424  fsumcvg2  14439  fsumsers  14440  fsumm1  14461  fsum1p  14463  fsumrev2  14495  telfsumo  14515  fsumparts  14519  cvgcmp  14529  cvgcmpub  14530  cvgcmpce  14531  isumsplit  14553  clim2prod  14601  clim2div  14602  prodfrec  14608  ntrivcvgtail  14613  fprodcvg  14641  fprodser  14660  fprodm1  14678  fprodeq0  14686  pcaddlem  15573  vdwnnlem2  15681  prmlem0  15793  gsumval2a  17260  telgsumfzs  18367  dvfsumle  23765  dvfsumge  23766  dvfsumabs  23767  coeid3  23977  ulmres  24123  ulmss  24132  chtdif  24865  ppidif  24870  bcmono  24983  axlowdimlem6  25808  extwwlkfablem2  27184  inffz  31589  inffzOLD  31590  mettrifi  33524  jm2.25  37385  jm2.16nn0  37390  dvgrat  38331  ssinc  39084  ssdec  39085  fzdifsuc2  39338  iuneqfzuzlem  39363  ssuzfz  39378  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  carageniuncllem1  40498  caratheodorylem1  40503
  Copyright terms: Public domain W3C validator