Theorem eluzel2 9014

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 9012	. . . 4 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2		frel 5159	. . . 4 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → Rel ℤ≥)
3	1, 2	ax-mp 7	. . 3 ⊢ Rel ℤ≥
4		relelfvdm 5330	. . 3 ⊢ ((Rel ℤ≥ ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ dom ℤ≥)
5	3, 4	mpan 415	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
6	1	fdmi 5162	. 2 ⊢ dom ℤ≥ = ℤ
7	5, 6	syl6eleq 2180	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1438  𝒫 cpw 3427  dom cdm 4436  Rel wrel 4441  ⟶wf 5006  ‘cfv 5010  ℤcz 8740  ℤ_≥cuz 9009

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3955  ax-pow 4007  ax-pr 4034  ax-cnex 7426  ax-resscn 7427

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2841  df-un 3003  df-in 3005  df-ss 3012  df-pw 3429  df-sn 3450  df-pr 3451  df-op 3453  df-uni 3652  df-br 3844  df-opab 3898  df-mpt 3899  df-id 4118  df-xp 4442  df-rel 4443  df-cnv 4444  df-co 4445  df-dm 4446  df-rn 4447  df-res 4448  df-ima 4449  df-iota 4975  df-fun 5012  df-fn 5013  df-f 5014  df-fv 5018  df-ov 5647  df-neg 7646  df-z 8741  df-uz 9010

This theorem is referenced by:  eluz2  9015  uztrn  9025  uzneg  9027  uzss  9029  uz11  9031  eluzadd  9037  uzm1  9039  uzin  9041  uzind4  9066  elfz5  9422  elfzel1  9429  eluzfz1  9435  fzsplit2  9454  fzopth  9464  fzpred  9472  fzpreddisj  9473  fzdifsuc  9483  uzsplit  9494  uzdisj  9495  elfzp12  9501  fzm1  9502  uznfz  9505  nn0disj  9537  fzolb  9552  fzoss2  9571  fzouzdisj  9579  ige2m2fzo  9597  elfzonelfzo  9629  frec2uzrand  9800  frecfzen2  9822  iseqcl  9869  iseqp1  9870  iseqp1t  9871  seq3p1  9872  seq3clss  9875  iseqfeq2  9879  seq3feq2  9881  iseqfveq  9882  seq3fveq  9883  iseqshft2  9886  seq3shft2  9887  seq3split  9895  iseqsplit  9896  iseqcaopr3  9898  seq3f1olemp  9919  seq3f1oleml  9920  seq3f1o  9921  ser3add  9923  iseqid3s  9926  iseqid  9927  iseqhomo  9930  iseqz  9931  seq3homo  9932  seq3distr  9934  ser0  9937  ser3ge0  9940  ser3le  9941  leexp2a  9996  hashfz  10217  hashfzo  10218  hashfzp1  10220  iseqcoll  10235  rexanuz2  10412  cau4  10537  clim2ser  10712  clim2ser2  10713  climserle  10721  fisumcvg  10753  fsum3cvg  10754  fisumcvg2  10773  fsum3cvg2  10774  fisumsers  10775  fisumser  10777  fsum3ser  10778  fsumm1  10797  fsum1p  10799  telfsumo  10847  fsumparts  10851  cvgcmpub  10857  isumsplit  10872  cvgratnnlemmn  10906  inffz  11800