Theorem eluzel2 11884

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

Syntax hints:   → wi 4   ∈ wcel 2139  𝒫 cpw 4302  dom cdm 5266  ‘cfv 6049  ℤcz 11569  ℤ_≥cuz 11879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-cnex 10184  ax-resscn 10185

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-neg 10461  df-z 11570  df-uz 11880

This theorem is referenced by:  eluz2  11885  uztrn  11896  uzneg  11898  uzss  11900  uz11  11902  eluzadd  11908  subeluzsub  11910  uzm1  11911  uzin  11913  uzind4  11939  uzsupss  11973  elfz5  12527  elfzel1  12534  eluzfz1  12541  fzsplit2  12559  fzopth  12571  ssfzunsn  12580  fzpred  12582  fzpreddisj  12583  uzsplit  12605  uzdisj  12606  fzm1  12613  uznfz  12616  nn0disj  12649  preduz  12655  fzolb  12670  fzoss2  12690  fzouzdisj  12698  fzoun  12699  ige2m2fzo  12725  fzen2  12962  seqp1  13010  seqcl  13015  seqfeq2  13018  seqfveq  13019  seqshft2  13021  seqsplit  13028  seqcaopr3  13030  seqf1olem2a  13033  seqf1olem1  13034  seqf1olem2  13035  seqid  13040  seqhomo  13042  seqz  13043  leexp2a  13110  hashfz  13406  fzsdom2  13407  hashfzo  13408  hashfzp1  13410  seqcoll  13440  rexanuz2  14288  cau4  14295  clim2ser  14584  clim2ser2  14585  climserle  14592  caurcvg  14606  caucvg  14608  fsumcvg  14642  fsumcvg2  14657  fsumsers  14658  fsumm1  14679  fsum1p  14681  fsumrev2  14713  telfsumo  14733  fsumparts  14737  cvgcmp  14747  cvgcmpub  14748  cvgcmpce  14749  isumsplit  14771  clim2prod  14819  clim2div  14820  prodfrec  14826  ntrivcvgtail  14831  fprodcvg  14859  fprodser  14878  fprodm1  14896  fprodeq0  14904  pcaddlem  15794  vdwnnlem2  15902  prmlem0  16014  gsumval2a  17480  telgsumfzs  18586  dvfsumle  23983  dvfsumge  23984  dvfsumabs  23985  coeid3  24195  ulmres  24341  ulmss  24350  chtdif  25083  ppidif  25088  bcmono  25201  axlowdimlem6  26026  inffz  31921  inffzOLD  31922  mettrifi  33866  jm2.25  38068  jm2.16nn0  38073  dvgrat  39013  ssinc  39763  ssdec  39764  fzdifsuc2  40023  iuneqfzuzlem  40048  ssuzfz  40063  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  carageniuncllem1  41241  caratheodorylem1  41246