Theorem eluzel2 12784

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

Syntax hints:   → wi 4   ∈ wcel 2119  𝒫 cpw 4529  dom cdm 5618  ‘cfv 6485  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  eluz2  12785  uztrn  12797  uzneg  12799  uzss  12802  uz11  12804  eluzadd  12808  subeluzsub  12812  uzm1  12813  uzin  12815  uzind4  12847  uzsupss  12881  elfz5  13461  elfzel1  13468  eluzfz1  13476  fzsplit2  13494  fzopth  13506  ssfzunsn  13515  fzpred  13517  fzpreddisj  13518  uzsplit  13541  uzdisj  13542  fzdif1  13550  fzm1  13552  uznfz  13555  nn0disj  13589  preduz  13595  fzolb  13611  fzoss2  13633  fzouzdisj  13641  fzoun  13642  ige2m2fzo  13674  fzen2  13922  seqp1  13969  seqcl  13975  seqfeq2  13978  seqfveq  13979  seqshft2  13981  seqsplit  13988  seqcaopr3  13990  seqf1olem2a  13993  seqf1olem1  13994  seqf1olem2  13995  seqid  14000  seqhomo  14002  seqz  14003  leexp2a  14125  hashfz  14380  fzsdom2  14381  hashfzo  14382  hashfzp1  14384  seqcoll  14417  rexanuz2  15303  cau4  15310  clim2ser  15608  clim2ser2  15609  climserle  15616  caurcvg  15630  caucvg  15632  fsumcvg  15665  fsumcvg2  15680  fsumsers  15681  fsumm1  15704  fsum1p  15706  fsumrev2  15735  telfsumo  15756  fsumparts  15760  cvgcmp  15770  cvgcmpub  15771  cvgcmpce  15772  isumsplit  15796  clim2prod  15844  clim2div  15845  prodfrec  15851  ntrivcvgtail  15856  fprodcvg  15886  fprodser  15905  fprodm1  15923  fprodeq0  15931  pcaddlem  16850  vdwnnlem2  16958  prmlem0  17067  gsumval2a  18644  telgsumfzs  19955  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  coeid3  26223  ulmres  26371  ulmss  26380  chtdif  27139  ppidif  27144  bcmono  27258  axlowdimlem6  29034  inffz  35958  mettrifi  38124  jm2.25  43444  jm2.16nn0  43449  dvgrat  44756  ssinc  45534  ssdec  45535  fzdifsuc2  45758  iuneqfzuzlem  45779  ssuzfz  45794  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  carageniuncllem1  46964  caratheodorylem1  46969