Theorem eluzel2 12754

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 6866	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 12752	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6671	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2844	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4552  dom cdm 5622  ‘cfv 6490  ℤcz 12486  ℤ_≥cuz 12749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487  df-uz 12750

This theorem is referenced by:  eluz2  12755  uztrn  12767  uzneg  12769  uzss  12772  uz11  12774  eluzadd  12778  subeluzsub  12782  uzm1  12783  uzin  12785  uzind4  12817  uzsupss  12851  elfz5  13430  elfzel1  13437  eluzfz1  13445  fzsplit2  13463  fzopth  13475  ssfzunsn  13484  fzpred  13486  fzpreddisj  13487  uzsplit  13510  uzdisj  13511  fzdif1  13519  fzm1  13521  uznfz  13524  nn0disj  13558  preduz  13564  fzolb  13579  fzoss2  13601  fzouzdisj  13609  fzoun  13610  ige2m2fzo  13642  fzen2  13890  seqp1  13937  seqcl  13943  seqfeq2  13946  seqfveq  13947  seqshft2  13949  seqsplit  13956  seqcaopr3  13958  seqf1olem2a  13961  seqf1olem1  13962  seqf1olem2  13963  seqid  13968  seqhomo  13970  seqz  13971  leexp2a  14093  hashfz  14348  fzsdom2  14349  hashfzo  14350  hashfzp1  14352  seqcoll  14385  rexanuz2  15271  cau4  15278  clim2ser  15576  clim2ser2  15577  climserle  15584  caurcvg  15598  caucvg  15600  fsumcvg  15633  fsumcvg2  15648  fsumsers  15649  fsumm1  15672  fsum1p  15674  fsumrev2  15703  telfsumo  15723  fsumparts  15727  cvgcmp  15737  cvgcmpub  15738  cvgcmpce  15739  isumsplit  15761  clim2prod  15809  clim2div  15810  prodfrec  15816  ntrivcvgtail  15821  fprodcvg  15851  fprodser  15870  fprodm1  15888  fprodeq0  15896  pcaddlem  16814  vdwnnlem2  16922  prmlem0  17031  gsumval2a  18608  telgsumfzs  19916  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  coeid3  26199  ulmres  26351  ulmss  26360  chtdif  27122  ppidif  27127  bcmono  27242  axlowdimlem6  28969  inffz  35873  mettrifi  37897  jm2.25  43183  jm2.16nn0  43188  dvgrat  44495  ssinc  45273  ssdec  45274  fzdifsuc2  45500  iuneqfzuzlem  45521  ssuzfz  45536  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  carageniuncllem1  46707  caratheodorylem1  46712