Theorem eluzel2 9653

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

Syntax hints:   → wi 4   ∈ wcel 2176  𝒫 cpw 3616  dom cdm 4675  Rel wrel 4680  ⟶wf 5267  ‘cfv 5271  ℤcz 9372  ℤ_≥cuz 9648

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-cnex 8016  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-mpt 4107  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373  df-uz 9649

This theorem is referenced by:  eluz2  9654  uztrn  9665  uzneg  9667  uzss  9669  uz11  9671  eluzadd  9677  uzm1  9679  uzin  9681  uzind4  9709  elfz5  10139  elfzel1  10146  eluzfz1  10153  fzsplit2  10172  fzopth  10183  fzpred  10192  fzpreddisj  10193  fzdifsuc  10203  uzsplit  10214  uzdisj  10215  elfzp12  10221  fzm1  10222  uznfz  10225  nn0disj  10260  fzolb  10276  fzoss2  10296  fzouzdisj  10304  ige2m2fzo  10327  elfzonelfzo  10359  frec2uzrand  10550  frecfzen2  10572  seq3p1  10610  seqp1cd  10615  seq3clss  10616  seq3feq2  10621  seqfveqg  10623  seq3fveq  10624  seq3shft2  10626  seqshft2g  10627  ser3mono  10632  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr2  10638  seq3f1olemp  10660  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem2a  10663  seqf1oglem1  10664  seqf1oglem2  10665  seqf1og  10666  seq3id3  10669  seq3id  10670  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  seq3distr  10677  ser3ge0  10681  ser3le  10682  leexp2a  10737  hashfz  10966  hashfzo  10967  hashfzp1  10969  seq3coll  10987  rexanuz2  11302  cau4  11427  clim2ser  11648  clim2ser2  11649  climserle  11656  fsum3cvg  11689  fsum3cvg2  11705  fsumsersdc  11706  fsum3ser  11708  fsumm1  11727  fsum1p  11729  telfsumo  11777  fsumparts  11781  cvgcmpub  11787  isumsplit  11802  cvgratnnlemmn  11836  clim2prod  11850  clim2divap  11851  prodfrecap  11857  prodfdivap  11858  ntrivcvgap  11859  fproddccvg  11883  fprodm1  11909  fprodabs  11927  fprodeq0  11928  uzwodc  12358  pcaddlem  12662  fngsum  13220  igsumvalx  13221  gsumfzval  13223  gsumval2  13229  gsumfzz  13327  gsumfzconst  13677  gsumfzfsumlemm  14349  inffz  16011