| 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 12871 | . . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
| 2 | 1 | ffvelcdmi 7078 | . . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ) |
| 3 | 2 | elpwid 4570 | . . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ) |
| 4 | 1 | fdmi 6717 | . . 3 ⊢ dom ℤ≥ = ℤ |
| 5 | 3, 4 | eleq2s 2880 | . 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
| 6 | ndmfv 6913 | . . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅) | |
| 7 | 0ss 4356 | . . 3 ⊢ ∅ ⊆ ℤ | |
| 8 | 6, 7 | eqsstrdi 3980 | . 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
| 9 | 5, 8 | pm2.61i 184 | 1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 ∈ wcel 2142 ⊆ wss 3904 ∅c0 4285 𝒫 cpw 4561 dom cdm 5660 ‘cfv 6536 ℤcz 12597 ℤ≥cuz 12868 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pr 5403 ax-cnex 11162 ax-resscn 11163 |
| This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rab 3416 df-v 3456 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5555 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-fv 6544 df-ov 7415 df-neg 11450 df-z 12598 df-uz 12869 |
| This theorem is used by: uzssre 12890 uzwo 12941 uzwo2 12942 infssuzle 12961 infssuzcl 12962 uzsupss 12970 uzwo3 12973 uzsup 13903 cau3 15414 caubnd 15417 limsupgre 15539 rlimclim 15604 climz 15607 climaddc1 15693 climmulc2 15695 climsubc1 15696 climsubc2 15697 climlec2 15717 isercolllem1 15723 isercolllem2 15724 isercoll 15726 caurcvg 15735 caucvg 15737 iseraltlem1 15740 iseraltlem2 15741 iseraltlem3 15742 summolem2a 15773 summolem2 15774 zsum 15776 fsumcvg3 15787 climfsum 15879 divcnvshft 15916 clim2prod 15949 ntrivcvg 15958 ntrivcvgfvn0 15960 ntrivcvgtail 15961 ntrivcvgmullem 15962 ntrivcvgmul 15963 prodrblem 15990 prodmolem2a 15995 prodmolem2 15996 zprod 15998 4sqlem11 17021 gsumval3 19983 lmbrf 23428 lmres 23468 uzrest 24065 uzfbas 24066 lmflf 24173 lmmbrf 25432 iscau4 25449 iscauf 25450 caucfil 25453 lmclimf 25474 mbfsup 25834 mbflimsup 25836 ig1pdvds 26348 ulmval 26554 ulmpm 26557 2sqlem6 27598 ballotlemfc0 34892 ballotlemfcc 34893 ballotlemiex 34901 ballotlemsima 34915 ballotlemrv2 34921 breprexplemc 35028 erdszelem4 35694 erdszelem8 35698 caures 38439 diophin 43531 irrapxlem1 43577 monotuz 43696 hashnzfzclim 45060 uzmptshftfval 45084 uzct 45811 uzfissfz 46070 ssuzfz 46093 uzssre2 46149 uzssz2 46198 uzinico2 46305 fnlimfvre 46416 climleltrp 46418 limsupequzmpt2 46460 limsupequzlem 46464 liminfequzmpt2 46533 ioodvbdlimc1lem2 46674 ioodvbdlimc2lem 46676 sge0isum 47169 smflimlem1 47513 smflimlem2 47514 smflim 47519 |
| Copyright terms: Public domain | W3C validator |