Theorem uzssz 12861

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 12843	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7065	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4565	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6704	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2881	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6900	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4355	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3981	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 183	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2143   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4556  dom cdm 5648  ‘cfv 6522  ℤcz 12569  ℤ_≥cuz 12840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-cnex 11130  ax-resscn 11131

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-fv 6530  df-ov 7400  df-neg 11418  df-z 12570  df-uz 12841

This theorem is referenced by:  uzssre  12862  uzwo  12913  uzwo2  12914  infssuzle  12933  infssuzcl  12934  uzsupss  12942  uzwo3  12945  uzsup  13874  cau3  15384  caubnd  15387  limsupgre  15509  rlimclim  15574  climz  15577  climaddc1  15663  climmulc2  15665  climsubc1  15666  climsubc2  15667  climlec2  15687  isercolllem1  15693  isercolllem2  15694  isercoll  15696  caurcvg  15705  caucvg  15707  iseraltlem1  15710  iseraltlem2  15711  iseraltlem3  15712  summolem2a  15743  summolem2  15744  zsum  15746  fsumcvg3  15757  climfsum  15849  divcnvshft  15886  clim2prod  15919  ntrivcvg  15928  ntrivcvgfvn0  15930  ntrivcvgtail  15931  ntrivcvgmullem  15932  ntrivcvgmul  15933  prodrblem  15960  prodmolem2a  15965  prodmolem2  15966  zprod  15968  4sqlem11  16992  gsumval3  19948  lmbrf  23321  lmres  23361  uzrest  23958  uzfbas  23959  lmflf  24066  lmmbrf  25325  iscau4  25342  iscauf  25343  caucfil  25346  lmclimf  25367  mbfsup  25727  mbflimsup  25729  ig1pdvds  26241  ulmval  26444  ulmpm  26447  2sqlem6  27488  ballotlemfc0  34791  ballotlemfcc  34792  ballotlemiex  34800  ballotlemsima  34814  ballotlemrv2  34820  breprexplemc  34927  erdszelem4  35545  erdszelem8  35549  caures  38260  diophin  43354  irrapxlem1  43400  monotuz  43519  hashnzfzclim  44899  uzmptshftfval  44923  uzct  45644  uzfissfz  45903  ssuzfz  45926  uzssre2  45982  uzssz2  46031  uzinico2  46138  fnlimfvre  46249  climleltrp  46251  limsupequzmpt2  46293  limsupequzlem  46297  liminfequzmpt2  46366  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  sge0isum  47002  smflimlem1  47346  smflimlem2  47347  smflim  47352