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

Theorem eluzel2 10485
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 5749 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  dom  ZZ>= )
2 uzf 10483 . . 3  |-  ZZ>= : ZZ --> ~P ZZ
32fdmi 5588 . 2  |-  dom  ZZ>=  =  ZZ
41, 3syl6eleq 2525 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   ~Pcpw 3791   dom cdm 4870   ` cfv 5446   ZZcz 10274   ZZ>=cuz 10480
This theorem is referenced by:  eluz2  10486  uztrn  10494  uzneg  10496  uzss  10498  uz11  10500  eluzadd  10506  uzm1  10508  uzin  10510  uzind4  10526  uzsupss  10560  elfz5  11043  elfzel1  11050  eluzfz1  11056  fzsplit2  11068  fzopth  11081  uzsplit  11110  uzdisj  11111  elfzp12  11118  fzm1  11119  uznfz  11122  fzolb  11137  fzoss2  11155  fzouzdisj  11161  fzen2  11300  seqp1  11330  seqcl  11335  seqfeq2  11338  seqfveq  11339  seqshft2  11341  seqsplit  11348  seqcaopr3  11350  seqf1olem2a  11353  seqf1olem1  11354  seqf1olem2  11355  seqid  11360  seqhomo  11362  seqz  11363  leexp2a  11427  hashfz  11684  fzsdom2  11685  hashfzo  11686  seqcoll  11704  rexanuz2  12145  cau4  12152  clim2ser  12440  clim2ser2  12441  climserle  12448  caurcvg  12462  caucvg  12464  fsumcvg  12498  fsumcvg2  12513  fsumsers  12514  fsumm1  12529  fsum1p  12531  fsumrev2  12557  fsumtscopo  12573  fsumparts  12577  cvgcmp  12587  cvgcmpub  12588  cvgcmpce  12589  isumsplit  12612  pcaddlem  13249  vdwnnlem2  13356  prmlem0  13420  gsumval2a  14774  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  coeid3  20151  ulmres  20296  ulmss  20305  chtdif  20933  ppidif  20938  bcmono  21053  inffz  25192  clim2prod  25208  clim2div  25209  prodfrec  25215  ntrivcvgtail  25220  fprodcvg  25248  fprodser  25267  fprodm1  25282  fprodeq0  25291  preduz  25467  axlowdimlem6  25878  mettrifi  26454  jm2.25  27061  jm2.16nn0  27066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-cnex 9038  ax-resscn 9039
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454  df-ov 6076  df-neg 9286  df-z 10275  df-uz 10481
  Copyright terms: Public domain W3C validator