Theorem eluzel2 9876

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

Syntax hints:   → wi 4   ∈ wcel 2205  𝒫 cpw 3674  dom cdm 4754  Rel wrel 4759  ⟶wf 5353  ‘cfv 5357  ℤcz 9594  ℤ_≥cuz 9871

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-cnex 8234  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595  df-uz 9872

This theorem is referenced by:  eluz2  9877  uztrn  9889  uzneg  9891  uzss  9893  uz11  9895  eluzadd  9901  uzm1  9903  uzin  9905  uzind4  9938  elfz5  10370  elfzel1  10377  eluzfz1  10385  fzsplit2  10404  fzopth  10416  fzpred  10426  fzpreddisj  10427  fzdifsuc  10437  uzsplit  10448  uzdisj  10449  elfzp12  10455  fzm1  10456  uznfz  10459  nn0disj  10494  fzolb  10510  fzoss2  10530  fzouzdisj  10538  fzoun  10539  ige2m2fzo  10565  elfzonelfzo  10597  frec2uzrand  10791  frecfzen2  10813  seq3p1  10851  seqp1cd  10856  seq3clss  10857  seq3feq2  10862  seqfveqg  10864  seq3fveq  10865  seq3shft2  10867  seqshft2g  10868  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem2a  10904  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  seq3id3  10910  seq3id  10911  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  ser3ge0  10922  ser3le  10923  leexp2a  10978  hashfz  11211  hashfzo  11212  hashfzp1  11214  seq3coll  11239  rexanuz2  11701  cau4  11826  clim2ser  12047  clim2ser2  12048  climserle  12055  fsum3cvg  12089  fsum3cvg2  12105  fsumsersdc  12106  fsum3ser  12108  fsumm1  12127  fsum1p  12129  telfsumo  12177  fsumparts  12181  cvgcmpub  12187  isumsplit  12202  cvgratnnlemmn  12236  clim2prod  12250  clim2divap  12251  prodfrecap  12257  prodfdivap  12258  ntrivcvgap  12259  fproddccvg  12283  fprodm1  12309  fprodabs  12327  fprodeq0  12328  uzwodc  12758  pcaddlem  13062  fngsum  13651  igsumvalx  13652  gsumfzval  13654  gsumval2  13660  gsumfzz  13750  gsumfzconst  14094  gsumshift  14105  gsumfzfsumlemm  14861  inffz  16984