Theorem eluzel2 12883

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

Syntax hints:   → wi 4   ∈ wcel 2108  𝒫 cpw 4600  dom cdm 5685  ‘cfv 6561  ℤcz 12613  ℤ_≥cuz 12878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  eluz2  12884  uztrn  12896  uzneg  12898  uzss  12901  uz11  12903  eluzadd  12907  eluzaddOLD  12913  subeluzsub  12915  uzm1  12916  uzin  12918  uzind4  12948  uzsupss  12982  elfz5  13556  elfzel1  13563  eluzfz1  13571  fzsplit2  13589  fzopth  13601  ssfzunsn  13610  fzpred  13612  fzpreddisj  13613  uzsplit  13636  uzdisj  13637  fzdif1  13645  fzm1  13647  uznfz  13650  nn0disj  13684  preduz  13690  fzolb  13705  fzoss2  13727  fzouzdisj  13735  fzoun  13736  ige2m2fzo  13767  fzen2  14010  seqp1  14057  seqcl  14063  seqfeq2  14066  seqfveq  14067  seqshft2  14069  seqsplit  14076  seqcaopr3  14078  seqf1olem2a  14081  seqf1olem1  14082  seqf1olem2  14083  seqid  14088  seqhomo  14090  seqz  14091  leexp2a  14212  hashfz  14466  fzsdom2  14467  hashfzo  14468  hashfzp1  14470  seqcoll  14503  rexanuz2  15388  cau4  15395  clim2ser  15691  clim2ser2  15692  climserle  15699  caurcvg  15713  caucvg  15715  fsumcvg  15748  fsumcvg2  15763  fsumsers  15764  fsumm1  15787  fsum1p  15789  fsumrev2  15818  telfsumo  15838  fsumparts  15842  cvgcmp  15852  cvgcmpub  15853  cvgcmpce  15854  isumsplit  15876  clim2prod  15924  clim2div  15925  prodfrec  15931  ntrivcvgtail  15936  fprodcvg  15966  fprodser  15985  fprodm1  16003  fprodeq0  16011  pcaddlem  16926  vdwnnlem2  17034  prmlem0  17143  gsumval2a  18698  telgsumfzs  20007  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  coeid3  26279  ulmres  26431  ulmss  26440  chtdif  27201  ppidif  27206  bcmono  27321  axlowdimlem6  28962  inffz  35730  mettrifi  37764  jm2.25  43011  jm2.16nn0  43016  dvgrat  44331  ssinc  45092  ssdec  45093  fzdifsuc2  45322  iuneqfzuzlem  45345  ssuzfz  45360  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  carageniuncllem1  46536  caratheodorylem1  46541