Theorem eluzel2 9546

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		uzf 9544	. . . 4 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2		frel 5382	. . . 4 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → Rel ℤ≥)
3	1, 2	ax-mp 5	. . 3 ⊢ Rel ℤ≥
4		relelfvdm 5559	. . 3 ⊢ ((Rel ℤ≥ ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ dom ℤ≥)
5	3, 4	mpan 424	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
6	1	fdmi 5385	. 2 ⊢ dom ℤ≥ = ℤ
7	5, 6	eleqtrdi 2280	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2158  𝒫 cpw 3587  dom cdm 4638  Rel wrel 4643  ⟶wf 5224  ‘cfv 5228  ℤcz 9266  ℤ_≥cuz 9541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-cnex 7915  ax-resscn 7916

This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-rab 2474  df-v 2751  df-sbc 2975  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-fv 5236  df-ov 5891  df-neg 8144  df-z 9267  df-uz 9542

This theorem is referenced by:  eluz2  9547  uztrn  9557  uzneg  9559  uzss  9561  uz11  9563  eluzadd  9569  uzm1  9571  uzin  9573  uzind4  9601  elfz5  10030  elfzel1  10037  eluzfz1  10044  fzsplit2  10063  fzopth  10074  fzpred  10083  fzpreddisj  10084  fzdifsuc  10094  uzsplit  10105  uzdisj  10106  elfzp12  10112  fzm1  10113  uznfz  10116  nn0disj  10151  fzolb  10166  fzoss2  10185  fzouzdisj  10193  ige2m2fzo  10211  elfzonelfzo  10243  frec2uzrand  10418  frecfzen2  10440  seq3p1  10475  seqp1cd  10479  seq3clss  10480  seq3feq2  10483  seq3fveq  10484  seq3shft2  10486  ser3mono  10491  seq3split  10492  seq3caopr3  10494  seq3caopr2  10495  seq3f1olemp  10515  seq3f1oleml  10516  seq3f1o  10517  seq3id3  10520  seq3id  10521  seq3homo  10523  seq3z  10524  seq3distr  10526  ser3ge0  10530  ser3le  10531  leexp2a  10586  hashfz  10814  hashfzo  10815  hashfzp1  10817  seq3coll  10835  rexanuz2  11013  cau4  11138  clim2ser  11358  clim2ser2  11359  climserle  11366  fsum3cvg  11399  fsum3cvg2  11415  fsumsersdc  11416  fsum3ser  11418  fsumm1  11437  fsum1p  11439  telfsumo  11487  fsumparts  11491  cvgcmpub  11497  isumsplit  11512  cvgratnnlemmn  11546  clim2prod  11560  clim2divap  11561  prodfrecap  11567  prodfdivap  11568  ntrivcvgap  11569  fproddccvg  11593  fprodm1  11619  fprodabs  11637  fprodeq0  11638  uzwodc  12051  pcaddlem  12351  inffz  15092