Theorem eluzel2 11692

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

Syntax hints:   → wi 4   ∈ wcel 1990  𝒫 cpw 4158  dom cdm 5114  ‘cfv 5888  ℤcz 11377  ℤ_≥cuz 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378  df-uz 11688

This theorem is referenced by:  eluz2  11693  uztrn  11704  uzneg  11706  uzss  11708  uz11  11710  eluzadd  11716  uzm1  11718  uzin  11720  uzind4  11746  uzsupss  11780  elfz5  12334  elfzel1  12341  eluzfz1  12348  fzsplit2  12366  fzopth  12378  ssfzunsn  12387  fzpred  12389  fzpreddisj  12390  uzsplit  12412  uzdisj  12413  fzm1  12420  uznfz  12423  nn0disj  12455  preduz  12461  fzolb  12476  fzoss2  12496  fzouzdisj  12504  ige2m2fzo  12530  fzen2  12768  seqp1  12816  seqcl  12821  seqfeq2  12824  seqfveq  12825  seqshft2  12827  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqf1olem1  12840  seqf1olem2  12841  seqid  12846  seqhomo  12848  seqz  12849  leexp2a  12916  hashfz  13214  fzsdom2  13215  hashfzo  13216  hashfzp1  13218  seqcoll  13248  rexanuz2  14089  cau4  14096  clim2ser  14385  clim2ser2  14386  climserle  14393  caurcvg  14407  caucvg  14409  fsumcvg  14443  fsumcvg2  14458  fsumsers  14459  fsumm1  14480  fsum1p  14482  fsumrev2  14514  telfsumo  14534  fsumparts  14538  cvgcmp  14548  cvgcmpub  14549  cvgcmpce  14550  isumsplit  14572  clim2prod  14620  clim2div  14621  prodfrec  14627  ntrivcvgtail  14632  fprodcvg  14660  fprodser  14679  fprodm1  14697  fprodeq0  14705  pcaddlem  15592  vdwnnlem2  15700  prmlem0  15812  gsumval2a  17279  telgsumfzs  18386  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  coeid3  23996  ulmres  24142  ulmss  24151  chtdif  24884  ppidif  24889  bcmono  25002  axlowdimlem6  25827  inffz  31614  inffzOLD  31615  mettrifi  33553  jm2.25  37566  jm2.16nn0  37571  dvgrat  38511  ssinc  39264  ssdec  39265  fzdifsuc2  39525  iuneqfzuzlem  39550  ssuzfz  39565  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  carageniuncllem1  40735  caratheodorylem1  40740