Theorem eluzel2 9804

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

Syntax hints:   → wi 4   ∈ wcel 2202  𝒫 cpw 3656  dom cdm 4731  Rel wrel 4736  ⟶wf 5329  ‘cfv 5333  ℤcz 9523  ℤ_≥cuz 9799

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-cnex 8166  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524  df-uz 9800

This theorem is referenced by:  eluz2  9805  uztrn  9817  uzneg  9819  uzss  9821  uz11  9823  eluzadd  9829  uzm1  9831  uzin  9833  uzind4  9866  elfz5  10297  elfzel1  10304  eluzfz1  10311  fzsplit2  10330  fzopth  10341  fzpred  10350  fzpreddisj  10351  fzdifsuc  10361  uzsplit  10372  uzdisj  10373  elfzp12  10379  fzm1  10380  uznfz  10383  nn0disj  10418  fzolb  10434  fzoss2  10454  fzouzdisj  10462  fzoun  10463  ige2m2fzo  10489  elfzonelfzo  10521  frec2uzrand  10713  frecfzen2  10735  seq3p1  10773  seqp1cd  10778  seq3clss  10779  seq3feq2  10784  seqfveqg  10786  seq3fveq  10787  seq3shft2  10789  seqshft2g  10790  ser3mono  10795  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seq3caopr2  10801  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem2a  10826  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  seq3id3  10832  seq3id  10833  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  seq3distr  10840  ser3ge0  10844  ser3le  10845  leexp2a  10900  hashfz  11131  hashfzo  11132  hashfzp1  11134  seq3coll  11152  rexanuz2  11614  cau4  11739  clim2ser  11960  clim2ser2  11961  climserle  11968  fsum3cvg  12002  fsum3cvg2  12018  fsumsersdc  12019  fsum3ser  12021  fsumm1  12040  fsum1p  12042  telfsumo  12090  fsumparts  12094  cvgcmpub  12100  isumsplit  12115  cvgratnnlemmn  12149  clim2prod  12163  clim2divap  12164  prodfrecap  12170  prodfdivap  12171  ntrivcvgap  12172  fproddccvg  12196  fprodm1  12222  fprodabs  12240  fprodeq0  12241  uzwodc  12671  pcaddlem  12975  fngsum  13534  igsumvalx  13535  gsumfzval  13537  gsumval2  13543  gsumfzz  13641  gsumfzconst  13991  gsumfzfsumlemm  14666  inffz  16788  gsumgfsumlem  16795