Theorem uzssz 12878

Description: An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
uzssz	⊢ (ℤ≥‘𝑀) ⊆ ℤ

Proof of Theorem uzssz

Step	Hyp	Ref	Expression
1		uzf 12860	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7078	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4571	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6717	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2881	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6913	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4357	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3981	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2143   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4562  dom cdm 5661  ‘cfv 6536  ℤcz 12586  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587  df-uz 12858

This theorem is referenced by:  uzssre  12879  uzwo  12930  uzwo2  12931  infssuzle  12950  infssuzcl  12951  uzsupss  12959  uzwo3  12962  uzsup  13892  cau3  15403  caubnd  15406  limsupgre  15528  rlimclim  15593  climz  15596  climaddc1  15682  climmulc2  15684  climsubc1  15685  climsubc2  15686  climlec2  15706  isercolllem1  15712  isercolllem2  15713  isercoll  15715  caurcvg  15724  caucvg  15726  iseraltlem1  15729  iseraltlem2  15730  iseraltlem3  15731  summolem2a  15762  summolem2  15763  zsum  15765  fsumcvg3  15776  climfsum  15868  divcnvshft  15905  clim2prod  15938  ntrivcvg  15947  ntrivcvgfvn0  15949  ntrivcvgtail  15950  ntrivcvgmullem  15951  ntrivcvgmul  15952  prodrblem  15979  prodmolem2a  15984  prodmolem2  15985  zprod  15987  4sqlem11  17010  gsumval3  19972  lmbrf  23417  lmres  23457  uzrest  24054  uzfbas  24055  lmflf  24162  lmmbrf  25421  iscau4  25438  iscauf  25439  caucfil  25442  lmclimf  25463  mbfsup  25823  mbflimsup  25825  ig1pdvds  26337  ulmval  26543  ulmpm  26546  2sqlem6  27587  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemiex  34892  ballotlemsima  34906  ballotlemrv2  34912  breprexplemc  35019  erdszelem4  35686  erdszelem8  35690  caures  38431  diophin  43523  irrapxlem1  43569  monotuz  43688  hashnzfzclim  45052  uzmptshftfval  45076  uzct  45803  uzfissfz  46062  ssuzfz  46085  uzssre2  46141  uzssz2  46190  uzinico2  46297  fnlimfvre  46408  climleltrp  46410  limsupequzmpt2  46452  limsupequzlem  46456  liminfequzmpt2  46525  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  sge0isum  47161  smflimlem1  47505  smflimlem2  47506  smflim  47511