Theorem uzssz 12911

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 12893	. . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
2	1	ffvelcdmi 7077	. . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ)
3	2	elpwid 4566	. . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ)
4	1	fdmi 6715	. . 3 ⊢ dom ℤ≥ = ℤ
5	3, 4	eleq2s 2878	. 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
6		ndmfv 6911	. . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
7		0ss 4350	. . 3 ⊢ ∅ ⊆ ℤ
8	6, 7	eqsstrdi 3975	. 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ)
9	5, 8	pm2.61i 184	1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  dom cdm 5655  ‘cfv 6533  ℤcz 12618  ℤ_≥cuz 12890

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-neg 11471  df-z 12619  df-uz 12891

This theorem is used by:  uzssre  12912  uzwo  12963  uzwo2  12964  infssuzle  12983  infssuzcl  12984  uzsupss  12992  uzwo3  12995  uzsup  13927  cau3  15446  caubnd  15449  limsupgre  15571  rlimclim  15636  climz  15639  climaddc1  15725  climmulc2  15727  climsubc1  15728  climsubc2  15729  climlec2  15749  isercolllem1  15755  isercolllem2  15756  isercoll  15758  caurcvg  15767  caucvg  15769  iseraltlem1  15772  iseraltlem2  15773  iseraltlem3  15774  summolem2a  15804  summolem2  15805  zsum  15807  fsumcvg3  15818  climfsum  15910  divcnvshft  15947  clim2prod  15980  ntrivcvg  15989  ntrivcvgfvn0  15991  ntrivcvgtail  15992  ntrivcvgmullem  15993  ntrivcvgmul  15994  prodrblem  16019  prodmolem2a  16024  prodmolem2  16025  zprod  16027  4sqlem11  17050  gsumval3  20037  lmbrf  23488  lmres  23528  uzrest  24126  uzfbas  24127  lmflf  24234  lmmbrf  25493  iscau4  25510  iscauf  25511  caucfil  25514  lmclimf  25535  mbfsup  25895  mbflimsup  25897  ig1pdvds  26408  ulmval  26619  ulmpm  26622  2sqlem6  27662  ballotlemfc0  35007  ballotlemfcc  35008  ballotlemiex  35016  ballotlemsima  35030  ballotlemrv2  35036  breprexplemc  35143  erdszelem4  35776  erdszelem8  35780  caures  38513  diophin  43620  irrapxlem1  43666  monotuz  43785  hashnzfzclim  45149  uzmptshftfval  45173  uzct  45900  uzfissfz  46159  ssuzfz  46182  uzssre2  46238  uzssz2  46287  uzinico2  46394  fnlimfvre  46505  climleltrp  46507  limsupequzmpt2  46549  limsupequzlem  46553  liminfequzmpt2  46622  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  sge0isum  47258  smflimlem1  47602  smflimlem2  47603  smflim  47608