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

Theorem eluzel2 11909
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 6440 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ dom ℤ)
2 uzf 11907 . . 3 :ℤ⟶𝒫 ℤ
32fdmi 6266 . 2 dom ℤ = ℤ
41, 3syl6eleq 2895 1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  𝒫 cpw 4351  dom cdm 5311  cfv 6101  cz 11643  cuz 11904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-cnex 10277  ax-resscn 10278
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6877  df-neg 10554  df-z 11644  df-uz 11905
This theorem is referenced by:  eluz2  11910  uztrn  11921  uzneg  11923  uzss  11925  uz11  11927  eluzadd  11933  subeluzsub  11935  uzm1  11936  uzin  11938  uzind4  11964  uzsupss  11999  elfz5  12557  elfzel1  12564  eluzfz1  12571  fzsplit2  12589  fzopth  12601  ssfzunsn  12610  fzpred  12612  fzpreddisj  12613  uzsplit  12635  uzdisj  12636  fzm1  12643  uznfz  12646  nn0disj  12679  preduz  12685  fzolb  12700  fzoss2  12720  fzouzdisj  12728  fzoun  12729  ige2m2fzo  12755  fzen2  12992  seqp1  13039  seqcl  13044  seqfeq2  13047  seqfveq  13048  seqshft2  13050  seqsplit  13057  seqcaopr3  13059  seqf1olem2a  13062  seqf1olem1  13063  seqf1olem2  13064  seqid  13069  seqhomo  13071  seqz  13072  leexp2a  13139  hashfz  13431  fzsdom2  13432  hashfzo  13433  hashfzp1  13435  seqcoll  13465  rexanuz2  14312  cau4  14319  clim2ser  14608  clim2ser2  14609  climserle  14616  caurcvg  14630  caucvg  14632  fsumcvg  14666  fsumcvg2  14681  fsumsers  14682  fsumm1  14703  fsum1p  14705  fsumrev2  14736  telfsumo  14756  fsumparts  14760  cvgcmp  14770  cvgcmpub  14771  cvgcmpce  14772  isumsplit  14794  clim2prod  14841  clim2div  14842  prodfrec  14848  ntrivcvgtail  14853  fprodcvg  14881  fprodser  14900  fprodm1  14918  fprodeq0  14926  pcaddlem  15809  vdwnnlem2  15917  prmlem0  16024  gsumval2a  17484  telgsumfzs  18588  dvfsumle  23998  dvfsumge  23999  dvfsumabs  24000  coeid3  24210  ulmres  24356  ulmss  24365  chtdif  25098  ppidif  25103  bcmono  25216  axlowdimlem6  26041  inffz  31936  inffzOLD  31937  mettrifi  33864  jm2.25  38067  jm2.16nn0  38072  dvgrat  39011  ssinc  39757  ssdec  39758  fzdifsuc2  40005  iuneqfzuzlem  40030  ssuzfz  40045  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  carageniuncllem1  41217  caratheodorylem1  41222
  Copyright terms: Public domain W3C validator