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

Theorem eluzel2 10869
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 5719 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  dom  ZZ>= )
2 uzf 10867 . . 3  |-  ZZ>= : ZZ --> ~P ZZ
32fdmi 5567 . 2  |-  dom  ZZ>=  =  ZZ
41, 3syl6eleq 2533 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   ~Pcpw 3863   dom cdm 4843   ` cfv 5421   ZZcz 10649   ZZ>=cuz 10864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-cnex 9341  ax-resscn 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6097  df-neg 9601  df-z 10650  df-uz 10865
This theorem is referenced by:  eluz2  10870  uztrn  10880  uzneg  10882  uzss  10884  uz11  10886  eluzadd  10892  uzm1  10894  uzin  10896  uzind4  10915  uzsupss  10950  elfz5  11448  elfzel1  11455  eluzfz1  11461  fzsplit2  11477  fzopth  11498  fzpred  11506  fzpreddisj  11507  uzsplit  11533  uzdisj  11534  elfzp12  11542  fzm1  11543  uznfz  11546  fzolb  11561  fzoss2  11580  fzouzdisj  11588  fzen2  11794  seqp1  11824  seqcl  11829  seqfeq2  11832  seqfveq  11833  seqshft2  11835  seqsplit  11842  seqcaopr3  11844  seqf1olem2a  11847  seqf1olem1  11848  seqf1olem2  11849  seqid  11854  seqhomo  11856  seqz  11857  leexp2a  11922  hashfz  12191  fzsdom2  12192  hashfzo  12193  seqcoll  12219  rexanuz2  12840  cau4  12847  clim2ser  13135  clim2ser2  13136  climserle  13143  caurcvg  13157  caucvg  13159  fsumcvg  13192  fsumcvg2  13207  fsumsers  13208  fsumm1  13223  fsum1p  13225  fsumrev2  13252  fsumtscopo  13268  fsumparts  13272  cvgcmp  13282  cvgcmpub  13283  cvgcmpce  13284  isumsplit  13306  pcaddlem  13953  vdwnnlem2  14060  prmlem0  14136  gsumval2a  15515  dvfsumle  21496  dvfsumge  21497  dvfsumabs  21498  coeid3  21711  ulmres  21856  ulmss  21865  chtdif  22499  ppidif  22504  bcmono  22619  axlowdimlem6  23196  inffz  27390  clim2prod  27406  clim2div  27407  prodfrec  27413  ntrivcvgtail  27418  fprodcvg  27446  fprodser  27465  fprodm1  27480  fprodeq0  27489  preduz  27664  mettrifi  28656  jm2.25  29351  jm2.16nn0  29356  el2fzo  30215  ige2m2fzo  30223  extwwlkfablem2  30674
  Copyright terms: Public domain W3C validator