Theorem eluzel2 12587

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

Syntax hints:   → wi 4   ∈ wcel 2106  𝒫 cpw 4533  dom cdm 5589  ‘cfv 6433  ℤcz 12319  ℤ_≥cuz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-neg 11208  df-z 12320  df-uz 12583

This theorem is referenced by:  eluz2  12588  uztrn  12600  uzneg  12602  uzss  12605  uz11  12607  eluzadd  12613  subeluzsub  12615  uzm1  12616  uzin  12618  uzind4  12646  uzsupss  12680  elfz5  13248  elfzel1  13255  eluzfz1  13263  fzsplit2  13281  fzopth  13293  ssfzunsn  13302  fzpred  13304  fzpreddisj  13305  uzsplit  13328  uzdisj  13329  fzm1  13336  uznfz  13339  nn0disj  13372  preduz  13378  fzolb  13393  fzoss2  13415  fzouzdisj  13423  fzoun  13424  ige2m2fzo  13450  fzen2  13689  seqp1  13736  seqcl  13743  seqfeq2  13746  seqfveq  13747  seqshft2  13749  seqsplit  13756  seqcaopr3  13758  seqf1olem2a  13761  seqf1olem1  13762  seqf1olem2  13763  seqid  13768  seqhomo  13770  seqz  13771  leexp2a  13890  hashfz  14142  fzsdom2  14143  hashfzo  14144  hashfzp1  14146  seqcoll  14178  rexanuz2  15061  cau4  15068  clim2ser  15366  clim2ser2  15367  climserle  15374  caurcvg  15388  caucvg  15390  fsumcvg  15424  fsumcvg2  15439  fsumsers  15440  fsumm1  15463  fsum1p  15465  fsumrev2  15494  telfsumo  15514  fsumparts  15518  cvgcmp  15528  cvgcmpub  15529  cvgcmpce  15530  isumsplit  15552  clim2prod  15600  clim2div  15601  prodfrec  15607  ntrivcvgtail  15612  fprodcvg  15640  fprodser  15659  fprodm1  15677  fprodeq0  15685  pcaddlem  16589  vdwnnlem2  16697  prmlem0  16807  gsumval2a  18369  telgsumfzs  19590  dvfsumle  25185  dvfsumge  25186  dvfsumabs  25187  coeid3  25401  ulmres  25547  ulmss  25556  chtdif  26307  ppidif  26312  bcmono  26425  axlowdimlem6  27315  inffz  33695  mettrifi  35915  jm2.25  40821  jm2.16nn0  40826  dvgrat  41930  ssinc  42637  ssdec  42638  fzdifsuc2  42849  iuneqfzuzlem  42873  ssuzfz  42888  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  carageniuncllem1  44059  caratheodorylem1  44064