Theorem eluzel2 12787

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

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4542  dom cdm 5625  ‘cfv 6493  ℤcz 12518  ℤ_≥cuz 12782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  eluz2  12788  uztrn  12800  uzneg  12802  uzss  12805  uz11  12807  eluzadd  12811  subeluzsub  12815  uzm1  12816  uzin  12818  uzind4  12850  uzsupss  12884  elfz5  13464  elfzel1  13471  eluzfz1  13479  fzsplit2  13497  fzopth  13509  ssfzunsn  13518  fzpred  13520  fzpreddisj  13521  uzsplit  13544  uzdisj  13545  fzdif1  13553  fzm1  13555  uznfz  13558  nn0disj  13592  preduz  13598  fzolb  13614  fzoss2  13636  fzouzdisj  13644  fzoun  13645  ige2m2fzo  13677  fzen2  13925  seqp1  13972  seqcl  13978  seqfeq2  13981  seqfveq  13982  seqshft2  13984  seqsplit  13991  seqcaopr3  13993  seqf1olem2a  13996  seqf1olem1  13997  seqf1olem2  13998  seqid  14003  seqhomo  14005  seqz  14006  leexp2a  14128  hashfz  14383  fzsdom2  14384  hashfzo  14385  hashfzp1  14387  seqcoll  14420  rexanuz2  15306  cau4  15313  clim2ser  15611  clim2ser2  15612  climserle  15619  caurcvg  15633  caucvg  15635  fsumcvg  15668  fsumcvg2  15683  fsumsers  15684  fsumm1  15707  fsum1p  15709  fsumrev2  15738  telfsumo  15759  fsumparts  15763  cvgcmp  15773  cvgcmpub  15774  cvgcmpce  15775  isumsplit  15799  clim2prod  15847  clim2div  15848  prodfrec  15854  ntrivcvgtail  15859  fprodcvg  15889  fprodser  15908  fprodm1  15926  fprodeq0  15934  pcaddlem  16853  vdwnnlem2  16961  prmlem0  17070  gsumval2a  18647  telgsumfzs  19958  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  coeid3  26218  ulmres  26369  ulmss  26378  chtdif  27138  ppidif  27143  bcmono  27257  axlowdimlem6  29033  inffz  35931  mettrifi  38095  jm2.25  43448  jm2.16nn0  43453  dvgrat  44760  ssinc  45538  ssdec  45539  fzdifsuc2  45764  iuneqfzuzlem  45785  ssuzfz  45800  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  carageniuncllem1  46970  caratheodorylem1  46975