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 ‘ 𝐴 ) ∈ ℝ )