Theorem uzssz 12252

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 12234	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelrni 6827	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4508	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6498	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2908	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6675	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4304	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3969	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 185	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2111   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  dom cdm 5519  ‘cfv 6324  ℤcz 11969  ℤ_≥cuz 12231

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970  df-uz 12232

This theorem is referenced by:  uzwo  12299  uzwo2  12300  infssuzle  12319  infssuzcl  12320  uzsupss  12328  uzwo3  12331  uzsup  13226  cau3  14707  caubnd  14710  limsupgre  14830  rlimclim  14895  climz  14898  climaddc1  14983  climmulc2  14985  climsubc1  14986  climsubc2  14987  climlec2  15007  isercolllem1  15013  isercolllem2  15014  isercoll  15016  caurcvg  15025  caucvg  15027  iseraltlem1  15030  iseraltlem2  15031  iseraltlem3  15032  summolem2a  15064  summolem2  15065  zsum  15067  fsumcvg3  15078  climfsum  15167  divcnvshft  15202  clim2prod  15236  ntrivcvg  15245  ntrivcvgfvn0  15247  ntrivcvgtail  15248  ntrivcvgmullem  15249  ntrivcvgmul  15250  prodrblem  15275  prodmolem2a  15280  prodmolem2  15281  zprod  15283  4sqlem11  16281  gsumval3  19020  lmbrf  21865  lmres  21905  uzrest  22502  uzfbas  22503  lmflf  22610  lmmbrf  23866  iscau4  23883  iscauf  23884  caucfil  23887  lmclimf  23908  mbfsup  24268  mbflimsup  24270  ig1pdvds  24777  ulmval  24975  ulmpm  24978  2sqlem6  26007  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemiex  31869  ballotlemsdom  31879  ballotlemsima  31883  ballotlemrv2  31889  breprexplemc  32013  erdszelem4  32554  erdszelem8  32558  caures  35198  diophin  39713  irrapxlem1  39763  monotuz  39882  hashnzfzclim  41026  uzmptshftfval  41050  uzct  41697  uzfissfz  41958  ssuzfz  41981  uzssre  42033  uzssre2  42044  uzssz2  42095  uzinico2  42199  fnlimfvre  42316  climleltrp  42318  limsupequzmpt2  42360  limsupequzlem  42364  liminfequzmpt2  42433  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  sge0isum  43066  smflimlem1  43404  smflimlem2  43405  smflim  43410