Theorem uzssz 12905

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 12887	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7102	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4619	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6743	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2847	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6940	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4407	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 4046	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2100   ⊆ wss 3959  ∅c0 4335  𝒫 cpw 4610  dom cdm 5686  ‘cfv 6558  ℤcz 12620  ℤ_≥cuz 12884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437  ax-cnex 11221  ax-resscn 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7433  df-neg 11504  df-z 12621  df-uz 12885

This theorem is referenced by:  uzssre  12906  uzwo  12957  uzwo2  12958  infssuzle  12977  infssuzcl  12978  uzsupss  12986  uzwo3  12989  uzsup  13894  cau3  15381  caubnd  15384  limsupgre  15504  rlimclim  15569  climz  15572  climaddc1  15658  climmulc2  15660  climsubc1  15661  climsubc2  15662  climlec2  15684  isercolllem1  15690  isercolllem2  15691  isercoll  15693  caurcvg  15702  caucvg  15704  iseraltlem1  15707  iseraltlem2  15708  iseraltlem3  15709  summolem2a  15740  summolem2  15741  zsum  15743  fsumcvg3  15754  climfsum  15845  divcnvshft  15880  clim2prod  15913  ntrivcvg  15922  ntrivcvgfvn0  15924  ntrivcvgtail  15925  ntrivcvgmullem  15926  ntrivcvgmul  15927  prodrblem  15952  prodmolem2a  15957  prodmolem2  15958  zprod  15960  4sqlem11  16978  gsumval3  19927  lmbrf  23278  lmres  23318  uzrest  23915  uzfbas  23916  lmflf  24023  lmmbrf  25304  iscau4  25321  iscauf  25322  caucfil  25325  lmclimf  25346  mbfsup  25707  mbflimsup  25709  ig1pdvds  26230  ulmval  26432  ulmpm  26435  2sqlem6  27475  ballotlemfc0  34364  ballotlemfcc  34365  ballotlemiex  34373  ballotlemsima  34387  ballotlemrv2  34393  breprexplemc  34516  erdszelem4  35069  erdszelem8  35073  caures  37508  diophin  42500  irrapxlem1  42550  monotuz  42670  hashnzfzclim  44067  uzmptshftfval  44091  uzct  44735  uzfissfz  45011  ssuzfz  45034  uzssre2  45092  uzssz2  45141  uzinico2  45250  fnlimfvre  45365  climleltrp  45367  limsupequzmpt2  45409  limsupequzlem  45413  liminfequzmpt2  45482  ioodvbdlimc1lem2  45623  ioodvbdlimc2lem  45625  sge0isum  46118  smflimlem1  46462  smflimlem2  46463  smflim  46468