Theorem uzssz 11129

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 11113	. . . . 5
2	1	ffvelrni 6030	. . . 4
3	2	elpwid 4022	. . 3
4	1	fdmi 5741	. . 3
5	3, 4	eleq2s 2565	. 2
6		ndmfv 5895	. . 3
7		0ss 3814	. . 3
8	6, 7	syl6eqss 3553	. 2
9	5, 8	pm2.61i 164	1

Syntax hints:  -.wn 3  e.wcel 1818  C_wss 3475  c0 3784  ~Pcpw 4012  domcdm 5004  `cfv 5593  cz 10889  cuz 11110

This theorem is referenced by:  uzwo  11173  uzwoOLD  11174  uzwo2  11175  uzinfmi  11190  infmssuzle  11193  infmssuzcl  11194  uzsupss  11203  uzwo3  11206  fzof  11826  uzsup  11990  cau3  13188  caubnd  13191  limsupgre  13304  rlimclim  13369  climz  13372  climaddc1  13457  climmulc2  13459  climsubc1  13460  climsubc2  13461  climlec2  13481  isercolllem1  13487  isercolllem2  13488  isercoll  13490  caurcvg  13499  caucvg  13501  iseraltlem1  13504  iseraltlem2  13505  iseraltlem3  13506  summolem2a  13537  summolem2  13538  zsum  13540  fsumcvg3  13551  climfsum  13634  clim2prod  13697  ntrivcvg  13706  ntrivcvgfvn0  13708  ntrivcvgtail  13709  ntrivcvgmullem  13710  ntrivcvgmul  13711  prodrblem  13736  prodmolem2a  13741  prodmolem2  13742  zprod  13744  4sqlem11  14473  gsumval3OLD  16908  gsumval3  16911  lmbrf  19761  lmres  19801  uzrest  20398  uzfbas  20399  lmflf  20506  lmmbrf  21701  iscau4  21718  iscauf  21719  caucfil  21722  lmclimf  21742  mbfsup  22071  mbflimsup  22073  ig1pdvds  22577  ulmval  22775  ulmpm  22778  2sqlem6  23644  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  ballotlemsdom  28450  ballotlemsima  28454  ballotlemrv2  28460  erdszelem4  28638  erdszelem8  28642  divcnvshft  29117  caures  30253  diophin  30706  irrapxlem1  30758  monotuz  30877  hashnzfzclim  31227  uzmptshftfval  31251  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-cnex 9569  ax-resscn 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890  df-uz 11111