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

Theorem eluzel2 10235
Description: Implication of membership in a set of upper 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 5554 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  dom  ZZ>= )
2 uzf 10233 . . 3  |-  ZZ>= : ZZ --> ~P ZZ
32fdmi 5394 . 2  |-  dom  ZZ>=  =  ZZ
41, 3syl6eleq 2373 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   ~Pcpw 3625   dom cdm 4689   ` cfv 5255   ZZcz 10024   ZZ>=cuz 10230
This theorem is referenced by:  eluz2  10236  uztrn  10244  uzneg  10246  uzss  10248  uz11  10250  eluzadd  10256  uzm1  10258  uzin  10260  uzind4  10276  uzsupss  10310  elfz5  10790  elfzel1  10797  eluzfz1  10803  fzsplit2  10815  fzopth  10828  uzsplit  10855  uzdisj  10856  elfzp12  10861  fzm1  10862  uznfz  10865  fzolb  10880  fzoss2  10897  fzouzdisj  10902  fzen2  11031  seqp1  11061  seqcl  11066  seqfeq2  11069  seqfveq  11070  seqshft2  11072  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqf1olem1  11085  seqf1olem2  11086  seqid  11091  seqhomo  11093  seqz  11094  leexp2a  11157  hashfz  11381  fzsdom2  11382  hashfzo  11383  seqcoll  11401  rexanuz2  11833  cau4  11840  clim2ser  12128  clim2ser2  12129  climserle  12136  caurcvg  12149  caucvg  12151  fsumcvg  12185  fsumcvg2  12200  fsumsers  12201  fsumm1  12216  fsum1p  12218  fsumrev2  12244  fsumtscopo  12260  fsumparts  12264  cvgcmp  12274  cvgcmpub  12275  cvgcmpce  12276  isumsplit  12299  pcaddlem  12936  vdwnnlem2  13043  prmlem0  13107  gsumval2a  14459  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  coeid3  19622  ulmres  19767  ulmss  19774  chtdif  20396  ppidif  20401  bcmono  20516  inffz  23506  preduz  23611  axlowdimlem6  23986  dffprod  24731  fprodser  24732  seqzp2  24767  mettrifi  25885  jm2.25  26504  jm2.16nn0  26509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-cnex 8793  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-ov 5861  df-neg 9040  df-z 10025  df-uz 10231
  Copyright terms: Public domain W3C validator