Theorem uzssz 12809

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 12791	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7035	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4550	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6679	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2854	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6872	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4340	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3966	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ⊆ wss 3889  ∅c0 4273  𝒫 cpw 4541  dom cdm 5631  ‘cfv 6498  ℤcz 12524  ℤ_≥cuz 12788

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-cnex 11094  ax-resscn 11095

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  uzssre  12810  uzwo  12861  uzwo2  12862  infssuzle  12881  infssuzcl  12882  uzsupss  12890  uzwo3  12893  uzsup  13822  cau3  15318  caubnd  15321  limsupgre  15443  rlimclim  15508  climz  15511  climaddc1  15597  climmulc2  15599  climsubc1  15600  climsubc2  15601  climlec2  15621  isercolllem1  15627  isercolllem2  15628  isercoll  15630  caurcvg  15639  caucvg  15641  iseraltlem1  15644  iseraltlem2  15645  iseraltlem3  15646  summolem2a  15677  summolem2  15678  zsum  15680  fsumcvg3  15691  climfsum  15783  divcnvshft  15820  clim2prod  15853  ntrivcvg  15862  ntrivcvgfvn0  15864  ntrivcvgtail  15865  ntrivcvgmullem  15866  ntrivcvgmul  15867  prodrblem  15894  prodmolem2a  15899  prodmolem2  15900  zprod  15902  4sqlem11  16926  gsumval3  19882  lmbrf  23225  lmres  23265  uzrest  23862  uzfbas  23863  lmflf  23970  lmmbrf  25229  iscau4  25246  iscauf  25247  caucfil  25250  lmclimf  25271  mbfsup  25631  mbflimsup  25633  ig1pdvds  26145  ulmval  26345  ulmpm  26348  2sqlem6  27386  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemiex  34646  ballotlemsima  34660  ballotlemrv2  34666  breprexplemc  34776  erdszelem4  35376  erdszelem8  35380  caures  38081  diophin  43204  irrapxlem1  43250  monotuz  43369  hashnzfzclim  44749  uzmptshftfval  44773  uzct  45494  uzfissfz  45756  ssuzfz  45779  uzssre2  45835  uzssz2  45884  uzinico2  45991  fnlimfvre  46102  climleltrp  46104  limsupequzmpt2  46146  limsupequzlem  46150  liminfequzmpt2  46219  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  sge0isum  46855  smflimlem1  47199  smflimlem2  47200  smflim  47205