Theorem eluzel2 11973

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

Syntax hints:   → wi 4   ∈ wcel 2164  𝒫 cpw 4378  dom cdm 5342  ‘cfv 6123  ℤcz 11704  ℤ_≥cuz 11968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-cnex 10308  ax-resscn 10309

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131  df-ov 6908  df-neg 10588  df-z 11705  df-uz 11969

This theorem is referenced by:  eluz2  11974  uztrn  11985  uzneg  11987  uzss  11989  uz11  11991  eluzadd  11997  subeluzsub  11999  uzm1  12000  uzin  12002  uzind4  12028  uzsupss  12063  elfz5  12627  elfzel1  12634  eluzfz1  12641  fzsplit2  12659  fzopth  12671  ssfzunsn  12680  fzpred  12682  fzpreddisj  12683  uzsplit  12706  uzdisj  12707  fzm1  12714  uznfz  12717  nn0disj  12750  preduz  12756  fzolb  12771  fzoss2  12791  fzouzdisj  12799  fzoun  12800  ige2m2fzo  12826  fzen2  13063  seqp1  13110  seqcl  13115  seqfeq2  13118  seqfveq  13119  seqshft2  13121  seqsplit  13128  seqcaopr3  13130  seqf1olem2a  13133  seqf1olem1  13134  seqf1olem2  13135  seqid  13140  seqhomo  13142  seqz  13143  leexp2a  13210  hashfz  13503  fzsdom2  13504  hashfzo  13505  hashfzp1  13507  seqcoll  13537  rexanuz2  14466  cau4  14473  clim2ser  14762  clim2ser2  14763  climserle  14770  caurcvg  14784  caucvg  14786  fsumcvg  14820  fsumcvg2  14835  fsumsers  14836  fsumm1  14857  fsum1p  14859  fsumrev2  14888  telfsumo  14908  fsumparts  14912  cvgcmp  14922  cvgcmpub  14923  cvgcmpce  14924  isumsplit  14946  clim2prod  14993  clim2div  14994  prodfrec  15000  ntrivcvgtail  15005  fprodcvg  15033  fprodser  15052  fprodm1  15070  fprodeq0  15078  pcaddlem  15963  vdwnnlem2  16071  prmlem0  16178  gsumval2a  17632  telgsumfzs  18740  dvfsumle  24183  dvfsumge  24184  dvfsumabs  24185  coeid3  24395  ulmres  24541  ulmss  24550  chtdif  25297  ppidif  25302  bcmono  25415  axlowdimlem6  26246  inffz  32146  mettrifi  34088  jm2.25  38402  jm2.16nn0  38407  dvgrat  39344  ssinc  40074  ssdec  40075  fzdifsuc2  40315  iuneqfzuzlem  40340  ssuzfz  40355  ioodvbdlimc1lem2  40935  ioodvbdlimc2lem  40937  carageniuncllem1  41522  caratheodorylem1  41527