![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzossfz | Structured version Visualization version GIF version |
Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
Ref | Expression |
---|---|
fzossfz | ⊢ (𝐴..^𝐵) ⊆ (𝐴...𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzofz 13585 | . 2 ⊢ (𝑥 ∈ (𝐴..^𝐵) → 𝑥 ∈ (𝐴...𝐵)) | |
2 | 1 | ssriv 3947 | 1 ⊢ (𝐴..^𝐵) ⊆ (𝐴...𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3909 (class class class)co 7354 ...cfz 13421 ..^cfzo 13564 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 ax-cnex 11104 ax-resscn 11105 ax-1cn 11106 ax-icn 11107 ax-addcl 11108 ax-addrcl 11109 ax-mulcl 11110 ax-mulrcl 11111 ax-mulcom 11112 ax-addass 11113 ax-mulass 11114 ax-distr 11115 ax-i2m1 11116 ax-1ne0 11117 ax-1rid 11118 ax-rnegex 11119 ax-rrecex 11120 ax-cnre 11121 ax-pre-lttri 11122 ax-pre-lttrn 11123 ax-pre-ltadd 11124 ax-pre-mulgt0 11125 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5530 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5587 df-we 5589 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6252 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7310 df-ov 7357 df-oprab 7358 df-mpo 7359 df-om 7800 df-1st 7918 df-2nd 7919 df-frecs 8209 df-wrecs 8240 df-recs 8314 df-rdg 8353 df-er 8645 df-en 8881 df-dom 8882 df-sdom 8883 df-pnf 11188 df-mnf 11189 df-xr 11190 df-ltxr 11191 df-le 11192 df-sub 11384 df-neg 11385 df-nn 12151 df-n0 12411 df-z 12497 df-uz 12761 df-fz 13422 df-fzo 13565 |
This theorem is referenced by: fzossz 13589 fzossnn0 13600 fzossnn 13618 elfzom1elp1fzo 13636 injresinjlem 13689 injresinj 13690 zmodfzp1 13797 uzindi 13884 wrdind 14607 wrd2ind 14608 scshwfzeqfzo 14712 telfsumo 15684 dfphi2 16643 cshwshashlem1 16965 psgnunilem5 19272 psgnunilem2 19273 efgredlemf 19519 efgredlemd 19522 efgredlemc 19523 uspgr2wlkeq 28492 wlkres 28516 redwlklem 28517 trlreslem 28545 pthdivtx 28575 eucrct2eupth 29087 cycpmfv2 31858 signstfvn 33072 signsvtn0 33073 breprexplemc 33136 pfxwlk 33608 fzossuz 43589 fourierdlem20 44338 fourierdlem25 44343 fourierdlem37 44355 fourierdlem64 44381 fourierdlem79 44396 fourierdlem89 44406 fourierdlem91 44408 fourierdlem101 44418 iccpartres 45580 iccpartipre 45583 iccpartleu 45590 bgoldbtbndlem2 45968 |
Copyright terms: Public domain | W3C validator |