Theorem uzssz 12873

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 12855	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7073	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4584	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6717	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2852	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6911	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4375	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 4003	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 182	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2108   ⊆ wss 3926  ∅c0 4308  𝒫 cpw 4575  dom cdm 5654  ‘cfv 6531  ℤcz 12588  ℤ_≥cuz 12852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-cnex 11185  ax-resscn 11186

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-neg 11469  df-z 12589  df-uz 12853

This theorem is referenced by:  uzssre  12874  uzwo  12927  uzwo2  12928  infssuzle  12947  infssuzcl  12948  uzsupss  12956  uzwo3  12959  uzsup  13880  cau3  15374  caubnd  15377  limsupgre  15497  rlimclim  15562  climz  15565  climaddc1  15651  climmulc2  15653  climsubc1  15654  climsubc2  15655  climlec2  15675  isercolllem1  15681  isercolllem2  15682  isercoll  15684  caurcvg  15693  caucvg  15695  iseraltlem1  15698  iseraltlem2  15699  iseraltlem3  15700  summolem2a  15731  summolem2  15732  zsum  15734  fsumcvg3  15745  climfsum  15836  divcnvshft  15871  clim2prod  15904  ntrivcvg  15913  ntrivcvgfvn0  15915  ntrivcvgtail  15916  ntrivcvgmullem  15917  ntrivcvgmul  15918  prodrblem  15945  prodmolem2a  15950  prodmolem2  15951  zprod  15953  4sqlem11  16975  gsumval3  19888  lmbrf  23198  lmres  23238  uzrest  23835  uzfbas  23836  lmflf  23943  lmmbrf  25214  iscau4  25231  iscauf  25232  caucfil  25235  lmclimf  25256  mbfsup  25617  mbflimsup  25619  ig1pdvds  26137  ulmval  26341  ulmpm  26344  2sqlem6  27386  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemiex  34534  ballotlemsima  34548  ballotlemrv2  34554  breprexplemc  34664  erdszelem4  35216  erdszelem8  35220  caures  37784  diophin  42795  irrapxlem1  42845  monotuz  42965  hashnzfzclim  44346  uzmptshftfval  44370  uzct  45087  uzfissfz  45353  ssuzfz  45376  uzssre2  45434  uzssz2  45483  uzinico2  45590  fnlimfvre  45703  climleltrp  45705  limsupequzmpt2  45747  limsupequzlem  45751  liminfequzmpt2  45820  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  sge0isum  46456  smflimlem1  46800  smflimlem2  46801  smflim  46806