Theorem eluzel2 12862

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4580  dom cdm 5659  ‘cfv 6536  ℤcz 12593  ℤ_≥cuz 12857

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-cnex 11190  ax-resscn 11191

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594  df-uz 12858

This theorem is referenced by:  eluz2  12863  uztrn  12875  uzneg  12877  uzss  12880  uz11  12882  eluzadd  12886  eluzaddOLD  12892  subeluzsub  12894  uzm1  12895  uzin  12897  uzind4  12927  uzsupss  12961  elfz5  13538  elfzel1  13545  eluzfz1  13553  fzsplit2  13571  fzopth  13583  ssfzunsn  13592  fzpred  13594  fzpreddisj  13595  uzsplit  13618  uzdisj  13619  fzdif1  13627  fzm1  13629  uznfz  13632  nn0disj  13666  preduz  13672  fzolb  13687  fzoss2  13709  fzouzdisj  13717  fzoun  13718  ige2m2fzo  13749  fzen2  13992  seqp1  14039  seqcl  14045  seqfeq2  14048  seqfveq  14049  seqshft2  14051  seqsplit  14058  seqcaopr3  14060  seqf1olem2a  14063  seqf1olem1  14064  seqf1olem2  14065  seqid  14070  seqhomo  14072  seqz  14073  leexp2a  14195  hashfz  14450  fzsdom2  14451  hashfzo  14452  hashfzp1  14454  seqcoll  14487  rexanuz2  15373  cau4  15380  clim2ser  15676  clim2ser2  15677  climserle  15684  caurcvg  15698  caucvg  15700  fsumcvg  15733  fsumcvg2  15748  fsumsers  15749  fsumm1  15772  fsum1p  15774  fsumrev2  15803  telfsumo  15823  fsumparts  15827  cvgcmp  15837  cvgcmpub  15838  cvgcmpce  15839  isumsplit  15861  clim2prod  15909  clim2div  15910  prodfrec  15916  ntrivcvgtail  15921  fprodcvg  15951  fprodser  15970  fprodm1  15988  fprodeq0  15996  pcaddlem  16913  vdwnnlem2  17021  prmlem0  17130  gsumval2a  18668  telgsumfzs  19975  dvfsumle  25983  dvfsumleOLD  25984  dvfsumge  25985  dvfsumabs  25986  coeid3  26202  ulmres  26354  ulmss  26363  chtdif  27125  ppidif  27130  bcmono  27245  axlowdimlem6  28931  inffz  35752  mettrifi  37786  jm2.25  42990  jm2.16nn0  42995  dvgrat  44303  ssinc  45078  ssdec  45079  fzdifsuc2  45306  iuneqfzuzlem  45328  ssuzfz  45343  ioodvbdlimc1lem2  45928  ioodvbdlimc2lem  45930  carageniuncllem1  46517  caratheodorylem1  46522