# 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 ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )

### Proof

Step Hyp Ref Expression
1 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
2 1 reseq1i ( [,) ↾ ( ℝ × ℝ ) ) = ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) )
3 ressxr ℝ ⊆ ℝ*
4 resmpo ( ( ℝ ⊆ ℝ* ∧ ℝ ⊆ ℝ* ) → ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) )
5 3 3 4 mp2an ( ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
6 2 5 eqtri ( [,) ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
7 6 rneqi ran ( [,) ↾ ( ℝ × ℝ ) ) = ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
8 7 eleq2i ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ 𝐴 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) )
9 8 biimpi ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → 𝐴 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) )
10 eqid ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
11 xrex * ∈ V
12 11 rabex { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ∈ V
13 10 12 elrnmpo ( 𝐴 ∈ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
14 9 13 sylib ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
15 simpr ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) → 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
16 3 sseli ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
17 16 adantr ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ* )
18 3 sseli ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
19 18 adantl ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ* )
20 icoval ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → ( 𝑥 [,) 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
21 17 19 20 syl2anc ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 [,) 𝑦 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
22 21 eqcomd ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } = ( 𝑥 [,) 𝑦 ) )
23 22 adantr ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) → { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } = ( 𝑥 [,) 𝑦 ) )
24 15 23 eqtrd ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } ) → 𝐴 = ( 𝑥 [,) 𝑦 ) )
25 24 ex ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } → 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
26 25 adantll ( ( ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } → 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
27 26 reximdva ( ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } → ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
28 27 reximdva ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) ) )
29 14 28 mpd ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) )
30 fveq2 ( 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) = ( vol ‘ ( 𝑥 [,) 𝑦 ) ) )
31 30 adantl ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 [,) 𝑦 ) ) → ( vol ‘ 𝐴 ) = ( vol ‘ ( 𝑥 [,) 𝑦 ) ) )
32 volicorecl ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( vol ‘ ( 𝑥 [,) 𝑦 ) ) ∈ ℝ )
33 32 adantr ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 [,) 𝑦 ) ) → ( vol ‘ ( 𝑥 [,) 𝑦 ) ) ∈ ℝ )
34 31 33 eqeltrd ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 [,) 𝑦 ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
35 34 ex ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) )
36 35 a1i ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) ) )
37 36 rexlimdvv ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) )
38 29 37 mpd ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
39 38 2a1d ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) ) )
40 39 rexlimdvv ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 [,) 𝑦 ) → ( vol ‘ 𝐴 ) ∈ ℝ ) )
41 29 40 mpd ( 𝐴 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )