Theorem eluzel2 12880

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

Syntax hints:   → wi 4   ∈ wcel 2105  𝒫 cpw 4604  dom cdm 5688  ‘cfv 6562  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  eluz2  12881  uztrn  12893  uzneg  12895  uzss  12898  uz11  12900  eluzadd  12904  eluzaddOLD  12910  subeluzsub  12912  uzm1  12913  uzin  12915  uzind4  12945  uzsupss  12979  elfz5  13552  elfzel1  13559  eluzfz1  13567  fzsplit2  13585  fzopth  13597  ssfzunsn  13606  fzpred  13608  fzpreddisj  13609  uzsplit  13632  uzdisj  13633  fzdif1  13641  fzm1  13643  uznfz  13646  nn0disj  13680  preduz  13686  fzolb  13701  fzoss2  13723  fzouzdisj  13731  fzoun  13732  ige2m2fzo  13763  fzen2  14006  seqp1  14053  seqcl  14059  seqfeq2  14062  seqfveq  14063  seqshft2  14065  seqsplit  14072  seqcaopr3  14074  seqf1olem2a  14077  seqf1olem1  14078  seqf1olem2  14079  seqid  14084  seqhomo  14086  seqz  14087  leexp2a  14208  hashfz  14462  fzsdom2  14463  hashfzo  14464  hashfzp1  14466  seqcoll  14499  rexanuz2  15384  cau4  15391  clim2ser  15687  clim2ser2  15688  climserle  15695  caurcvg  15709  caucvg  15711  fsumcvg  15744  fsumcvg2  15759  fsumsers  15760  fsumm1  15783  fsum1p  15785  fsumrev2  15814  telfsumo  15834  fsumparts  15838  cvgcmp  15848  cvgcmpub  15849  cvgcmpce  15850  isumsplit  15872  clim2prod  15920  clim2div  15921  prodfrec  15927  ntrivcvgtail  15932  fprodcvg  15962  fprodser  15981  fprodm1  15999  fprodeq0  16007  pcaddlem  16921  vdwnnlem2  17029  prmlem0  17139  gsumval2a  18710  telgsumfzs  20021  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  coeid3  26293  ulmres  26445  ulmss  26454  chtdif  27215  ppidif  27220  bcmono  27335  axlowdimlem6  28976  inffz  35709  mettrifi  37743  jm2.25  42987  jm2.16nn0  42992  dvgrat  44307  ssinc  45026  ssdec  45027  fzdifsuc2  45260  iuneqfzuzlem  45283  ssuzfz  45298  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  carageniuncllem1  46476  caratheodorylem1  46481