Theorem uzssz 12803

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 12785	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7030	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4551	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6674	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2855	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6867	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4341	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3967	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542  dom cdm 5625  ‘cfv 6493  ℤcz 12518  ℤ_≥cuz 12782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  uzssre  12804  uzwo  12855  uzwo2  12856  infssuzle  12875  infssuzcl  12876  uzsupss  12884  uzwo3  12887  uzsup  13816  cau3  15312  caubnd  15315  limsupgre  15437  rlimclim  15502  climz  15505  climaddc1  15591  climmulc2  15593  climsubc1  15594  climsubc2  15595  climlec2  15615  isercolllem1  15621  isercolllem2  15622  isercoll  15624  caurcvg  15633  caucvg  15635  iseraltlem1  15638  iseraltlem2  15639  iseraltlem3  15640  summolem2a  15671  summolem2  15672  zsum  15674  fsumcvg3  15685  climfsum  15777  divcnvshft  15814  clim2prod  15847  ntrivcvg  15856  ntrivcvgfvn0  15858  ntrivcvgtail  15859  ntrivcvgmullem  15860  ntrivcvgmul  15861  prodrblem  15888  prodmolem2a  15893  prodmolem2  15894  zprod  15896  4sqlem11  16920  gsumval3  19876  lmbrf  23238  lmres  23278  uzrest  23875  uzfbas  23876  lmflf  23983  lmmbrf  25242  iscau4  25259  iscauf  25260  caucfil  25263  lmclimf  25284  mbfsup  25644  mbflimsup  25646  ig1pdvds  26158  ulmval  26361  ulmpm  26364  2sqlem6  27403  ballotlemfc0  34656  ballotlemfcc  34657  ballotlemiex  34665  ballotlemsima  34679  ballotlemrv2  34685  breprexplemc  34795  erdszelem4  35395  erdszelem8  35399  caures  38098  diophin  43221  irrapxlem1  43271  monotuz  43390  hashnzfzclim  44770  uzmptshftfval  44794  uzct  45515  uzfissfz  45777  ssuzfz  45800  uzssre2  45856  uzssz2  45905  uzinico2  46012  fnlimfvre  46123  climleltrp  46125  limsupequzmpt2  46167  limsupequzlem  46171  liminfequzmpt2  46240  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  sge0isum  46876  smflimlem1  47220  smflimlem2  47221  smflim  47226