Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uzssz | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
uzssz | ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzf 12235 | . . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
2 | 1 | ffvelrni 6843 | . . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ) |
3 | 2 | elpwid 4551 | . . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ) |
4 | 1 | fdmi 6518 | . . 3 ⊢ dom ℤ≥ = ℤ |
5 | 3, 4 | eleq2s 2931 | . 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
6 | ndmfv 6694 | . . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅) | |
7 | 0ss 4349 | . . 3 ⊢ ∅ ⊆ ℤ | |
8 | 6, 7 | eqsstrdi 4020 | . 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
9 | 5, 8 | pm2.61i 183 | 1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2105 ⊆ wss 3935 ∅c0 4290 𝒫 cpw 4537 dom cdm 5549 ‘cfv 6349 ℤcz 11970 ℤ≥cuz 12232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-cnex 10582 ax-resscn 10583 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 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 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-fv 6357 df-ov 7148 df-neg 10862 df-z 11971 df-uz 12233 |
This theorem is referenced by: uzwo 12300 uzwo2 12301 infssuzle 12320 infssuzcl 12321 uzsupss 12329 uzwo3 12332 uzsup 13221 cau3 14705 caubnd 14708 limsupgre 14828 rlimclim 14893 climz 14896 climaddc1 14981 climmulc2 14983 climsubc1 14984 climsubc2 14985 climlec2 15005 isercolllem1 15011 isercolllem2 15012 isercoll 15014 caurcvg 15023 caucvg 15025 iseraltlem1 15028 iseraltlem2 15029 iseraltlem3 15030 summolem2a 15062 summolem2 15063 zsum 15065 fsumcvg3 15076 climfsum 15165 divcnvshft 15200 clim2prod 15234 ntrivcvg 15243 ntrivcvgfvn0 15245 ntrivcvgtail 15246 ntrivcvgmullem 15247 ntrivcvgmul 15248 prodrblem 15273 prodmolem2a 15278 prodmolem2 15279 zprod 15281 4sqlem11 16281 gsumval3 18958 lmbrf 21798 lmres 21838 uzrest 22435 uzfbas 22436 lmflf 22543 lmmbrf 23794 iscau4 23811 iscauf 23812 caucfil 23815 lmclimf 23836 mbfsup 24194 mbflimsup 24196 ig1pdvds 24699 ulmval 24897 ulmpm 24900 2sqlem6 25927 ballotlemfc0 31650 ballotlemfcc 31651 ballotlemiex 31659 ballotlemsdom 31669 ballotlemsima 31673 ballotlemrv2 31679 breprexplemc 31803 erdszelem4 32339 erdszelem8 32343 caures 34918 diophin 39249 irrapxlem1 39299 monotuz 39418 hashnzfzclim 40534 uzmptshftfval 40558 uzct 41205 uzfissfz 41474 ssuzfz 41497 uzssre 41549 uzssre2 41560 uzssz2 41612 uzinico2 41718 fnlimfvre 41835 climleltrp 41837 limsupequzmpt2 41879 limsupequzlem 41883 liminfequzmpt2 41952 ioodvbdlimc1lem2 42097 ioodvbdlimc2lem 42099 sge0isum 42590 smflimlem1 42928 smflimlem2 42929 smflim 42934 |
Copyright terms: Public domain | W3C validator |