Theorem eluzel2 12756

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

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4554  dom cdm 5624  ‘cfv 6492  ℤcz 12488  ℤ_≥cuz 12751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489  df-uz 12752

This theorem is referenced by:  eluz2  12757  uztrn  12769  uzneg  12771  uzss  12774  uz11  12776  eluzadd  12780  subeluzsub  12784  uzm1  12785  uzin  12787  uzind4  12819  uzsupss  12853  elfz5  13432  elfzel1  13439  eluzfz1  13447  fzsplit2  13465  fzopth  13477  ssfzunsn  13486  fzpred  13488  fzpreddisj  13489  uzsplit  13512  uzdisj  13513  fzdif1  13521  fzm1  13523  uznfz  13526  nn0disj  13560  preduz  13566  fzolb  13581  fzoss2  13603  fzouzdisj  13611  fzoun  13612  ige2m2fzo  13644  fzen2  13892  seqp1  13939  seqcl  13945  seqfeq2  13948  seqfveq  13949  seqshft2  13951  seqsplit  13958  seqcaopr3  13960  seqf1olem2a  13963  seqf1olem1  13964  seqf1olem2  13965  seqid  13970  seqhomo  13972  seqz  13973  leexp2a  14095  hashfz  14350  fzsdom2  14351  hashfzo  14352  hashfzp1  14354  seqcoll  14387  rexanuz2  15273  cau4  15280  clim2ser  15578  clim2ser2  15579  climserle  15586  caurcvg  15600  caucvg  15602  fsumcvg  15635  fsumcvg2  15650  fsumsers  15651  fsumm1  15674  fsum1p  15676  fsumrev2  15705  telfsumo  15725  fsumparts  15729  cvgcmp  15739  cvgcmpub  15740  cvgcmpce  15741  isumsplit  15763  clim2prod  15811  clim2div  15812  prodfrec  15818  ntrivcvgtail  15823  fprodcvg  15853  fprodser  15872  fprodm1  15890  fprodeq0  15898  pcaddlem  16816  vdwnnlem2  16924  prmlem0  17033  gsumval2a  18610  telgsumfzs  19918  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  coeid3  26201  ulmres  26353  ulmss  26362  chtdif  27124  ppidif  27129  bcmono  27244  axlowdimlem6  29020  inffz  35924  mettrifi  37958  jm2.25  43251  jm2.16nn0  43256  dvgrat  44563  ssinc  45341  ssdec  45342  fzdifsuc2  45568  iuneqfzuzlem  45589  ssuzfz  45604  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  carageniuncllem1  46775  caratheodorylem1  46780