Theorem eluzel2 9723

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 9721	. . . 4 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2		frel 5477	. . . 4 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → Rel ℤ≥)
3	1, 2	ax-mp 5	. . 3 ⊢ Rel ℤ≥
4		relelfvdm 5658	. . 3 ⊢ ((Rel ℤ≥ ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ dom ℤ≥)
5	3, 4	mpan 424	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
6	1	fdmi 5480	. 2 ⊢ dom ℤ≥ = ℤ
7	5, 6	eleqtrdi 2322	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2200  𝒫 cpw 3649  dom cdm 4718  Rel wrel 4723  ⟶wf 5313  ‘cfv 5317  ℤcz 9442  ℤ_≥cuz 9718

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-cnex 8086  ax-resscn 8087

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-fv 5325  df-ov 6003  df-neg 8316  df-z 9443  df-uz 9719

This theorem is referenced by:  eluz2  9724  uztrn  9735  uzneg  9737  uzss  9739  uz11  9741  eluzadd  9747  uzm1  9749  uzin  9751  uzind4  9779  elfz5  10209  elfzel1  10216  eluzfz1  10223  fzsplit2  10242  fzopth  10253  fzpred  10262  fzpreddisj  10263  fzdifsuc  10273  uzsplit  10284  uzdisj  10285  elfzp12  10291  fzm1  10292  uznfz  10295  nn0disj  10330  fzolb  10346  fzoss2  10366  fzouzdisj  10374  fzoun  10375  ige2m2fzo  10399  elfzonelfzo  10431  frec2uzrand  10622  frecfzen2  10644  seq3p1  10682  seqp1cd  10687  seq3clss  10688  seq3feq2  10693  seqfveqg  10695  seq3fveq  10696  seq3shft2  10698  seqshft2g  10699  ser3mono  10704  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seq3caopr2  10710  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem2a  10735  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  seq3id3  10741  seq3id  10742  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  seq3distr  10749  ser3ge0  10753  ser3le  10754  leexp2a  10809  hashfz  11038  hashfzo  11039  hashfzp1  11041  seq3coll  11059  rexanuz2  11497  cau4  11622  clim2ser  11843  clim2ser2  11844  climserle  11851  fsum3cvg  11884  fsum3cvg2  11900  fsumsersdc  11901  fsum3ser  11903  fsumm1  11922  fsum1p  11924  telfsumo  11972  fsumparts  11976  cvgcmpub  11982  isumsplit  11997  cvgratnnlemmn  12031  clim2prod  12045  clim2divap  12046  prodfrecap  12052  prodfdivap  12053  ntrivcvgap  12054  fproddccvg  12078  fprodm1  12104  fprodabs  12122  fprodeq0  12123  uzwodc  12553  pcaddlem  12857  fngsum  13416  igsumvalx  13417  gsumfzval  13419  gsumval2  13425  gsumfzz  13523  gsumfzconst  13873  gsumfzfsumlemm  14545  inffz  16399