Theorem eluzel2 12862

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

Step	Hyp	Ref	Expression
1		elfvdm 6915	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 12860	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6717	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2873	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2143  𝒫 cpw 4562  dom cdm 5661  ‘cfv 6536  ℤcz 12586  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587  df-uz 12858

This theorem is referenced by:  eluz2  12863  uztrn  12875  uzneg  12877  uzss  12880  uz11  12882  eluzadd  12886  subeluzsub  12890  uzm1  12891  uzin  12893  uzind4  12925  uzsupss  12959  elfz5  13539  elfzel1  13546  eluzfz1  13554  fzsplit2  13573  fzopth  13585  ssfzunsn  13594  fzpred  13596  fzpreddisj  13597  uzsplit  13620  uzdisj  13621  fzdif1  13629  fzm1  13631  uznfz  13634  nn0disj  13668  preduz  13674  fzolb  13690  fzoss2  13712  fzouzdisj  13720  fzoun  13721  ige2m2fzo  13753  fzen2  14001  seqp1  14048  seqcl  14054  seqfeq2  14057  seqfveq  14058  seqshft2  14060  seqsplit  14067  seqcaopr3  14069  seqf1olem2a  14072  seqf1olem1  14073  seqf1olem2  14074  seqid  14079  seqhomo  14081  seqz  14082  leexp2a  14204  hashfz  14460  fzsdom2  14461  hashfzo  14462  hashfzp1  14464  seqcoll  14497  rexanuz2  15397  cau4  15404  clim2ser  15702  clim2ser2  15703  climserle  15710  caurcvg  15724  caucvg  15726  fsumcvg  15759  fsumcvg2  15774  fsumsers  15775  fsumm1  15798  fsum1p  15800  fsumrev2  15829  telfsumo  15850  fsumparts  15854  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  isumsplit  15890  clim2prod  15938  clim2div  15939  prodfrec  15945  ntrivcvgtail  15950  fprodcvg  15980  fprodser  15999  fprodm1  16017  fprodeq0  16025  pcaddlem  16943  vdwnnlem2  17051  prmlem0  17160  gsumval2a  18738  telgsumfzs  20054  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  coeid3  26397  ulmres  26551  ulmss  26560  chtdif  27322  ppidif  27327  bcmono  27441  axlowdimlem6  29297  inffz  36222  mettrifi  38428  jm2.25  43746  jm2.16nn0  43751  dvgrat  45042  ssinc  45825  ssdec  45826  fzdifsuc2  46049  iuneqfzuzlem  46070  ssuzfz  46085  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  carageniuncllem1  47255  caratheodorylem1  47260