Theorem uzssz 12265

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 12247	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelrni 6850	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4550	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6524	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2931	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6700	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4350	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 4021	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

Syntax hints:  ¬ wn 3   ∈ wcel 2114   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  dom cdm 5555  ‘cfv 6355  ℤcz 11982  ℤ_≥cuz 12244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983  df-uz 12245

This theorem is referenced by:  uzwo  12312  uzwo2  12313  infssuzle  12332  infssuzcl  12333  uzsupss  12341  uzwo3  12344  uzsup  13232  cau3  14715  caubnd  14718  limsupgre  14838  rlimclim  14903  climz  14906  climaddc1  14991  climmulc2  14993  climsubc1  14994  climsubc2  14995  climlec2  15015  isercolllem1  15021  isercolllem2  15022  isercoll  15024  caurcvg  15033  caucvg  15035  iseraltlem1  15038  iseraltlem2  15039  iseraltlem3  15040  summolem2a  15072  summolem2  15073  zsum  15075  fsumcvg3  15086  climfsum  15175  divcnvshft  15210  clim2prod  15244  ntrivcvg  15253  ntrivcvgfvn0  15255  ntrivcvgtail  15256  ntrivcvgmullem  15257  ntrivcvgmul  15258  prodrblem  15283  prodmolem2a  15288  prodmolem2  15289  zprod  15291  4sqlem11  16291  gsumval3  19027  lmbrf  21868  lmres  21908  uzrest  22505  uzfbas  22506  lmflf  22613  lmmbrf  23865  iscau4  23882  iscauf  23883  caucfil  23886  lmclimf  23907  mbfsup  24265  mbflimsup  24267  ig1pdvds  24770  ulmval  24968  ulmpm  24971  2sqlem6  25999  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemiex  31759  ballotlemsdom  31769  ballotlemsima  31773  ballotlemrv2  31779  breprexplemc  31903  erdszelem4  32441  erdszelem8  32445  caures  35050  diophin  39389  irrapxlem1  39439  monotuz  39558  hashnzfzclim  40674  uzmptshftfval  40698  uzct  41345  uzfissfz  41614  ssuzfz  41637  uzssre  41689  uzssre2  41700  uzssz2  41752  uzinico2  41858  fnlimfvre  41975  climleltrp  41977  limsupequzmpt2  42019  limsupequzlem  42023  liminfequzmpt2  42092  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  sge0isum  42729  smflimlem1  43067  smflimlem2  43068  smflim  43073