Theorem icoresmbl

Description: A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	icoresmbl	⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ dom vol

Proof

Step	Hyp	Ref	Expression
1		elicores	⊢ ( 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑥 = ( 𝑦 [,) 𝑧 ) )
2	1	biimpi	⊢ ( 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑥 = ( 𝑦 [,) 𝑧 ) )
3		simpr	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 = ( 𝑦 [,) 𝑧 ) ) → 𝑥 = ( 𝑦 [,) 𝑧 ) )
4		simpl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑦 ∈ ℝ )
5		rexr	⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℝ* )
6	5	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ* )
7		icombl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ* ) → ( 𝑦 [,) 𝑧 ) ∈ dom vol )
8	4 6 7	syl2anc	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 [,) 𝑧 ) ∈ dom vol )
9	8	adantr	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 = ( 𝑦 [,) 𝑧 ) ) → ( 𝑦 [,) 𝑧 ) ∈ dom vol )
10	3 9	eqeltrd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 = ( 𝑦 [,) 𝑧 ) ) → 𝑥 ∈ dom vol )
11	10	rexlimdva2	⊢ ( 𝑦 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ 𝑥 = ( 𝑦 [,) 𝑧 ) → 𝑥 ∈ dom vol ) )
12	11	rexlimiv	⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑥 = ( 𝑦 [,) 𝑧 ) → 𝑥 ∈ dom vol )
13	12	a1i	⊢ ( 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → ( ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ 𝑥 = ( 𝑦 [,) 𝑧 ) → 𝑥 ∈ dom vol ) )
14	2 13	mpd	⊢ ( 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) → 𝑥 ∈ dom vol )
15	14	rgen	⊢ ∀ 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) 𝑥 ∈ dom vol
16		dfss3	⊢ ( ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ dom vol ↔ ∀ 𝑥 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) 𝑥 ∈ dom vol )
17	15 16	mpbir	⊢ ran ( [,) ↾ ( ℝ × ℝ ) ) ⊆ dom vol