![]() |
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 12906 | . . . . 5 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
2 | 1 | ffvelcdmi 7117 | . . . 4 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ∈ 𝒫 ℤ) |
3 | 2 | elpwid 4631 | . . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ ℤ) |
4 | 1 | fdmi 6758 | . . 3 ⊢ dom ℤ≥ = ℤ |
5 | 3, 4 | eleq2s 2862 | . 2 ⊢ (𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
6 | ndmfv 6955 | . . 3 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅) | |
7 | 0ss 4423 | . . 3 ⊢ ∅ ⊆ ℤ | |
8 | 6, 7 | eqsstrdi 4063 | . 2 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) ⊆ ℤ) |
9 | 5, 8 | pm2.61i 182 | 1 ⊢ (ℤ≥‘𝑀) ⊆ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2108 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 dom cdm 5700 ‘cfv 6573 ℤcz 12639 ℤ≥cuz 12903 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-cnex 11240 ax-resscn 11241 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-fv 6581 df-ov 7451 df-neg 11523 df-z 12640 df-uz 12904 |
This theorem is referenced by: uzssre 12925 uzwo 12976 uzwo2 12977 infssuzle 12996 infssuzcl 12997 uzsupss 13005 uzwo3 13008 uzsup 13914 cau3 15404 caubnd 15407 limsupgre 15527 rlimclim 15592 climz 15595 climaddc1 15681 climmulc2 15683 climsubc1 15684 climsubc2 15685 climlec2 15707 isercolllem1 15713 isercolllem2 15714 isercoll 15716 caurcvg 15725 caucvg 15727 iseraltlem1 15730 iseraltlem2 15731 iseraltlem3 15732 summolem2a 15763 summolem2 15764 zsum 15766 fsumcvg3 15777 climfsum 15868 divcnvshft 15903 clim2prod 15936 ntrivcvg 15945 ntrivcvgfvn0 15947 ntrivcvgtail 15948 ntrivcvgmullem 15949 ntrivcvgmul 15950 prodrblem 15977 prodmolem2a 15982 prodmolem2 15983 zprod 15985 4sqlem11 17002 gsumval3 19949 lmbrf 23289 lmres 23329 uzrest 23926 uzfbas 23927 lmflf 24034 lmmbrf 25315 iscau4 25332 iscauf 25333 caucfil 25336 lmclimf 25357 mbfsup 25718 mbflimsup 25720 ig1pdvds 26239 ulmval 26441 ulmpm 26444 2sqlem6 27485 ballotlemfc0 34457 ballotlemfcc 34458 ballotlemiex 34466 ballotlemsima 34480 ballotlemrv2 34486 breprexplemc 34609 erdszelem4 35162 erdszelem8 35166 caures 37720 diophin 42728 irrapxlem1 42778 monotuz 42898 hashnzfzclim 44291 uzmptshftfval 44315 uzct 44965 uzfissfz 45241 ssuzfz 45264 uzssre2 45322 uzssz2 45371 uzinico2 45480 fnlimfvre 45595 climleltrp 45597 limsupequzmpt2 45639 limsupequzlem 45643 liminfequzmpt2 45712 ioodvbdlimc1lem2 45853 ioodvbdlimc2lem 45855 sge0isum 46348 smflimlem1 46692 smflimlem2 46693 smflim 46698 |
Copyright terms: Public domain | W3C validator |