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

Theorem eluzel2 10862
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  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )

Proof of Theorem eluzel2
StepHypRef Expression
1 elfvdm 5713 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  dom  ZZ>= )
2 uzf 10860 . . 3  |-  ZZ>= : ZZ --> ~P ZZ
32fdmi 5561 . 2  |-  dom  ZZ>=  =  ZZ
41, 3syl6eleq 2531 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   ~Pcpw 3857   dom cdm 4836   ` cfv 5415   ZZcz 10642   ZZ>=cuz 10857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-cnex 9334  ax-resscn 9335
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fv 5423  df-ov 6093  df-neg 9594  df-z 10643  df-uz 10858
This theorem is referenced by:  eluz2  10863  uztrn  10873  uzneg  10875  uzss  10877  uz11  10879  eluzadd  10885  uzm1  10887  uzin  10889  uzind4  10908  uzsupss  10943  elfz5  11441  elfzel1  11448  eluzfz1  11454  fzsplit2  11470  fzopth  11491  fzpred  11499  fzpreddisj  11500  uzsplit  11526  uzdisj  11527  elfzp12  11535  fzm1  11536  uznfz  11539  fzolb  11554  fzoss2  11573  fzouzdisj  11581  fzen2  11787  seqp1  11817  seqcl  11822  seqfeq2  11825  seqfveq  11826  seqshft2  11828  seqsplit  11835  seqcaopr3  11837  seqf1olem2a  11840  seqf1olem1  11841  seqf1olem2  11842  seqid  11847  seqhomo  11849  seqz  11850  leexp2a  11915  hashfz  12184  fzsdom2  12185  hashfzo  12186  seqcoll  12212  rexanuz2  12833  cau4  12840  clim2ser  13128  clim2ser2  13129  climserle  13136  caurcvg  13150  caucvg  13152  fsumcvg  13185  fsumcvg2  13200  fsumsers  13201  fsumm1  13216  fsum1p  13218  fsumrev2  13245  fsumtscopo  13261  fsumparts  13265  cvgcmp  13275  cvgcmpub  13276  cvgcmpce  13277  isumsplit  13299  pcaddlem  13946  vdwnnlem2  14053  prmlem0  14129  gsumval2a  15505  dvfsumle  21452  dvfsumge  21453  dvfsumabs  21454  coeid3  21667  ulmres  21812  ulmss  21821  chtdif  22455  ppidif  22460  bcmono  22575  axlowdimlem6  23128  inffz  27316  clim2prod  27332  clim2div  27333  prodfrec  27339  ntrivcvgtail  27344  fprodcvg  27372  fprodser  27391  fprodm1  27406  fprodeq0  27415  preduz  27590  mettrifi  28578  jm2.25  29273  jm2.16nn0  29278  el2fzo  30137  ige2m2fzo  30145  extwwlkfablem2  30596
  Copyright terms: Public domain W3C validator