Theorem eluzel2 12774

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4559  dom cdm 5631  ‘cfv 6499  ℤcz 12505  ℤ_≥cuz 12769

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506  df-uz 12770

This theorem is referenced by:  eluz2  12775  uztrn  12787  uzneg  12789  uzss  12792  uz11  12794  eluzadd  12798  eluzaddOLD  12804  subeluzsub  12806  uzm1  12807  uzin  12809  uzind4  12841  uzsupss  12875  elfz5  13453  elfzel1  13460  eluzfz1  13468  fzsplit2  13486  fzopth  13498  ssfzunsn  13507  fzpred  13509  fzpreddisj  13510  uzsplit  13533  uzdisj  13534  fzdif1  13542  fzm1  13544  uznfz  13547  nn0disj  13581  preduz  13587  fzolb  13602  fzoss2  13624  fzouzdisj  13632  fzoun  13633  ige2m2fzo  13665  fzen2  13910  seqp1  13957  seqcl  13963  seqfeq2  13966  seqfveq  13967  seqshft2  13969  seqsplit  13976  seqcaopr3  13978  seqf1olem2a  13981  seqf1olem1  13982  seqf1olem2  13983  seqid  13988  seqhomo  13990  seqz  13991  leexp2a  14113  hashfz  14368  fzsdom2  14369  hashfzo  14370  hashfzp1  14372  seqcoll  14405  rexanuz2  15292  cau4  15299  clim2ser  15597  clim2ser2  15598  climserle  15605  caurcvg  15619  caucvg  15621  fsumcvg  15654  fsumcvg2  15669  fsumsers  15670  fsumm1  15693  fsum1p  15695  fsumrev2  15724  telfsumo  15744  fsumparts  15748  cvgcmp  15758  cvgcmpub  15759  cvgcmpce  15760  isumsplit  15782  clim2prod  15830  clim2div  15831  prodfrec  15837  ntrivcvgtail  15842  fprodcvg  15872  fprodser  15891  fprodm1  15909  fprodeq0  15917  pcaddlem  16835  vdwnnlem2  16943  prmlem0  17052  gsumval2a  18594  telgsumfzs  19903  dvfsumle  25959  dvfsumleOLD  25960  dvfsumge  25961  dvfsumabs  25962  coeid3  26178  ulmres  26330  ulmss  26339  chtdif  27101  ppidif  27106  bcmono  27221  axlowdimlem6  28927  inffz  35710  mettrifi  37744  jm2.25  42981  jm2.16nn0  42986  dvgrat  44294  ssinc  45074  ssdec  45075  fzdifsuc2  45301  iuneqfzuzlem  45323  ssuzfz  45338  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  carageniuncllem1  46512  caratheodorylem1  46517