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 11566 | . . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
2 | 1 | ffvelrni 6266 | . . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ) |
3 | 2 | elpwid 4118 | . . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ) |
4 | 1 | fdmi 5965 | . . 3 ⊢ dom ℤ≥ = ℤ |
5 | 3, 4 | eleq2s 2706 | . 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
6 | ndmfv 6128 | . . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅) | |
7 | 0ss 3924 | . . 3 ⊢ ∅ ⊆ ℤ | |
8 | 6, 7 | syl6eqss 3618 | . 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
9 | 5, 8 | pm2.61i 175 | 1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 1977 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 dom cdm 5038 ‘cfv 5804 ℤcz 11254 ℤ≥cuz 11563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-cnex 9871 ax-resscn 9872 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-ov 6552 df-neg 10148 df-z 11255 df-uz 11564 |
This theorem is referenced by: uzwo 11627 uzwo2 11628 infssuzle 11647 infssuzcl 11648 uzsupss 11656 uzwo3 11659 fzof 12336 uzsup 12524 cau3 13943 caubnd 13946 limsupgre 14060 rlimclim 14125 climz 14128 climaddc1 14213 climmulc2 14215 climsubc1 14216 climsubc2 14217 climlec2 14237 isercolllem1 14243 isercolllem2 14244 isercoll 14246 caurcvg 14255 caucvg 14257 iseraltlem1 14260 iseraltlem2 14261 iseraltlem3 14262 summolem2a 14293 summolem2 14294 zsum 14296 fsumcvg3 14307 climfsum 14393 divcnvshft 14426 clim2prod 14459 ntrivcvg 14468 ntrivcvgfvn0 14470 ntrivcvgtail 14471 ntrivcvgmullem 14472 ntrivcvgmul 14473 prodrblem 14498 prodmolem2a 14503 prodmolem2 14504 zprod 14506 4sqlem11 15497 gsumval3 18131 lmbrf 20874 lmres 20914 uzrest 21511 uzfbas 21512 lmflf 21619 lmmbrf 22868 iscau4 22885 iscauf 22886 caucfil 22889 lmclimf 22910 mbfsup 23237 mbflimsup 23239 ig1pdvds 23740 ulmval 23938 ulmpm 23941 2sqlem6 24948 ballotlemfc0 29881 ballotlemfcc 29882 ballotlemiex 29890 ballotlemsdom 29900 ballotlemsima 29904 ballotlemrv2 29910 erdszelem4 30430 erdszelem8 30434 caures 32726 diophin 36354 irrapxlem1 36404 monotuz 36524 hashnzfzclim 37543 uzmptshftfval 37567 uzct 38257 uzfissfz 38483 ssuzfz 38506 fnlimfvre 38741 climleltrp 38743 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 sge0isum 39320 smflimlem1 39657 smflimlem2 39658 smflim 39663 |
Copyright terms: Public domain | W3C validator |