Theorem eluzel2 9759

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

Syntax hints:   → wi 4   ∈ wcel 2202  𝒫 cpw 3652  dom cdm 4725  Rel wrel 4730  ⟶wf 5322  ‘cfv 5326  ℤcz 9478  ℤ_≥cuz 9754

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-cnex 8122  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479  df-uz 9755

This theorem is referenced by:  eluz2  9760  uztrn  9772  uzneg  9774  uzss  9776  uz11  9778  eluzadd  9784  uzm1  9786  uzin  9788  uzind4  9821  elfz5  10251  elfzel1  10258  eluzfz1  10265  fzsplit2  10284  fzopth  10295  fzpred  10304  fzpreddisj  10305  fzdifsuc  10315  uzsplit  10326  uzdisj  10327  elfzp12  10333  fzm1  10334  uznfz  10337  nn0disj  10372  fzolb  10388  fzoss2  10408  fzouzdisj  10416  fzoun  10417  ige2m2fzo  10442  elfzonelfzo  10474  frec2uzrand  10666  frecfzen2  10688  seq3p1  10726  seqp1cd  10731  seq3clss  10732  seq3feq2  10737  seqfveqg  10739  seq3fveq  10740  seq3shft2  10742  seqshft2g  10743  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem2a  10779  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  seq3id3  10785  seq3id  10786  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  ser3ge0  10797  ser3le  10798  leexp2a  10853  hashfz  11084  hashfzo  11085  hashfzp1  11087  seq3coll  11105  rexanuz2  11551  cau4  11676  clim2ser  11897  clim2ser2  11898  climserle  11905  fsum3cvg  11938  fsum3cvg2  11954  fsumsersdc  11955  fsum3ser  11957  fsumm1  11976  fsum1p  11978  telfsumo  12026  fsumparts  12030  cvgcmpub  12036  isumsplit  12051  cvgratnnlemmn  12085  clim2prod  12099  clim2divap  12100  prodfrecap  12106  prodfdivap  12107  ntrivcvgap  12108  fproddccvg  12132  fprodm1  12158  fprodabs  12176  fprodeq0  12177  uzwodc  12607  pcaddlem  12911  fngsum  13470  igsumvalx  13471  gsumfzval  13473  gsumval2  13479  gsumfzz  13577  gsumfzconst  13927  gsumfzfsumlemm  14600  inffz  16676  gsumgfsumlem  16683