# Metamath Proof Explorer

## Theorem volicorescl

Description: The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion volicorescl ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to vol\left({A}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 df-ico ${⊢}\left[.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
2 1 reseq1i ${⊢}{\left[.\right)↾}_{{ℝ}^{2}}={\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)↾}_{{ℝ}^{2}}$
3 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
4 resmpo ${⊢}\left(ℝ\subseteq {ℝ}^{*}\wedge ℝ\subseteq {ℝ}^{*}\right)\to {\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
5 3 3 4 mp2an ${⊢}{\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
6 2 5 eqtri ${⊢}{\left[.\right)↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
7 6 rneqi ${⊢}\mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)=\mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
8 7 eleq2i ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)↔{A}\in \mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
9 8 biimpi ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to {A}\in \mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
10 eqid ${⊢}\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)=\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
11 xrex ${⊢}{ℝ}^{*}\in \mathrm{V}$
12 11 rabex ${⊢}\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\in \mathrm{V}$
13 10 12 elrnmpo ${⊢}{A}\in \mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}$
14 9 13 sylib ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}$
15 simpr ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)\to {A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}$
16 3 sseli ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
17 16 adantr ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}\in {ℝ}^{*}$
18 3 sseli ${⊢}{y}\in ℝ\to {y}\in {ℝ}^{*}$
19 18 adantl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {y}\in {ℝ}^{*}$
20 icoval ${⊢}\left({x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left[{x},{y}\right)=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}$
21 17 19 20 syl2anc ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left[{x},{y}\right)=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}$
22 21 eqcomd ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}=\left[{x},{y}\right)$
23 22 adantr ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)\to \left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}=\left[{x},{y}\right)$
24 15 23 eqtrd ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)\to {A}=\left[{x},{y}\right)$
25 24 ex ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\to {A}=\left[{x},{y}\right)\right)$
26 25 adantll ${⊢}\left(\left({A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\wedge {x}\in ℝ\right)\wedge {y}\in ℝ\right)\to \left({A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\to {A}=\left[{x},{y}\right)\right)$
27 26 reximdva ${⊢}\left({A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\wedge {x}\in ℝ\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left[{x},{y}\right)\right)$
28 27 reximdva ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left[{x},{y}\right)\right)$
29 14 28 mpd ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left[{x},{y}\right)$
30 fveq2 ${⊢}{A}=\left[{x},{y}\right)\to vol\left({A}\right)=vol\left(\left[{x},{y}\right)\right)$
31 30 adantl ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left[{x},{y}\right)\right)\to vol\left({A}\right)=vol\left(\left[{x},{y}\right)\right)$
32 volicorecl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to vol\left(\left[{x},{y}\right)\right)\in ℝ$
33 32 adantr ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left[{x},{y}\right)\right)\to vol\left(\left[{x},{y}\right)\right)\in ℝ$
34 31 33 eqeltrd ${⊢}\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {A}=\left[{x},{y}\right)\right)\to vol\left({A}\right)\in ℝ$
35 34 ex ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}=\left[{x},{y}\right)\to vol\left({A}\right)\in ℝ\right)$
36 35 a1i ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}=\left[{x},{y}\right)\to vol\left({A}\right)\in ℝ\right)\right)$
37 36 rexlimdvv ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left[{x},{y}\right)\to vol\left({A}\right)\in ℝ\right)$
38 29 37 mpd ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to vol\left({A}\right)\in ℝ$
39 38 2a1d ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}=\left[{x},{y}\right)\to vol\left({A}\right)\in ℝ\right)\right)$
40 39 rexlimdvv ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}=\left[{x},{y}\right)\to vol\left({A}\right)\in ℝ\right)$
41 29 40 mpd ${⊢}{A}\in \mathrm{ran}\left({\left[.\right)↾}_{{ℝ}^{2}}\right)\to vol\left({A}\right)\in ℝ$