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 12240 | . . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
2 | 1 | ffvelrni 6844 | . . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ) |
3 | 2 | elpwid 4552 | . . 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 184 | 1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2110 ⊆ wss 3935 ∅c0 4290 𝒫 cpw 4538 dom cdm 5549 ‘cfv 6349 ℤcz 11975 ℤ≥cuz 12237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-cnex 10587 ax-resscn 10588 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 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 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 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 7153 df-neg 10867 df-z 11976 df-uz 12238 |
This theorem is referenced by: uzwo 12305 uzwo2 12306 infssuzle 12325 infssuzcl 12326 uzsupss 12334 uzwo3 12337 uzsup 13225 cau3 14709 caubnd 14712 limsupgre 14832 rlimclim 14897 climz 14900 climaddc1 14985 climmulc2 14987 climsubc1 14988 climsubc2 14989 climlec2 15009 isercolllem1 15015 isercolllem2 15016 isercoll 15018 caurcvg 15027 caucvg 15029 iseraltlem1 15032 iseraltlem2 15033 iseraltlem3 15034 summolem2a 15066 summolem2 15067 zsum 15069 fsumcvg3 15080 climfsum 15169 divcnvshft 15204 clim2prod 15238 ntrivcvg 15247 ntrivcvgfvn0 15249 ntrivcvgtail 15250 ntrivcvgmullem 15251 ntrivcvgmul 15252 prodrblem 15277 prodmolem2a 15282 prodmolem2 15283 zprod 15285 4sqlem11 16285 gsumval3 19021 lmbrf 21862 lmres 21902 uzrest 22499 uzfbas 22500 lmflf 22607 lmmbrf 23859 iscau4 23876 iscauf 23877 caucfil 23880 lmclimf 23901 mbfsup 24259 mbflimsup 24261 ig1pdvds 24764 ulmval 24962 ulmpm 24965 2sqlem6 25993 ballotlemfc0 31745 ballotlemfcc 31746 ballotlemiex 31754 ballotlemsdom 31764 ballotlemsima 31768 ballotlemrv2 31774 breprexplemc 31898 erdszelem4 32436 erdszelem8 32440 caures 35029 diophin 39362 irrapxlem1 39412 monotuz 39531 hashnzfzclim 40647 uzmptshftfval 40671 uzct 41318 uzfissfz 41587 ssuzfz 41610 uzssre 41662 uzssre2 41673 uzssz2 41725 uzinico2 41831 fnlimfvre 41948 climleltrp 41950 limsupequzmpt2 41992 limsupequzlem 41996 liminfequzmpt2 42065 ioodvbdlimc1lem2 42210 ioodvbdlimc2lem 42212 sge0isum 42703 smflimlem1 43041 smflimlem2 43042 smflim 43047 |
Copyright terms: Public domain | W3C validator |