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 ( [,) |` ( RR X. RR ) ) C_ dom vol

Proof

Step	Hyp	Ref	Expression
1		elicores	|- ( x e. ran ( [,) |` ( RR X. RR ) ) <-> E. y e. RR E. z e. RR x = ( y [,) z ) )
2	1	biimpi	|- ( x e. ran ( [,) |` ( RR X. RR ) ) -> E. y e. RR E. z e. RR x = ( y [,) z ) )
3		simpr	|- ( ( ( y e. RR /\ z e. RR ) /\ x = ( y [,) z ) ) -> x = ( y [,) z ) )
4		simpl	|- ( ( y e. RR /\ z e. RR ) -> y e. RR )
5		rexr	|- ( z e. RR -> z e. RR* )
6	5	adantl	|- ( ( y e. RR /\ z e. RR ) -> z e. RR* )
7		icombl	|- ( ( y e. RR /\ z e. RR* ) -> ( y [,) z ) e. dom vol )
8	4 6 7	syl2anc	|- ( ( y e. RR /\ z e. RR ) -> ( y [,) z ) e. dom vol )
9	8	adantr	|- ( ( ( y e. RR /\ z e. RR ) /\ x = ( y [,) z ) ) -> ( y [,) z ) e. dom vol )
10	3 9	eqeltrd	|- ( ( ( y e. RR /\ z e. RR ) /\ x = ( y [,) z ) ) -> x e. dom vol )
11	10	rexlimdva2	|- ( y e. RR -> ( E. z e. RR x = ( y [,) z ) -> x e. dom vol ) )
12	11	rexlimiv	|- ( E. y e. RR E. z e. RR x = ( y [,) z ) -> x e. dom vol )
13	12	a1i	|- ( x e. ran ( [,) |` ( RR X. RR ) ) -> ( E. y e. RR E. z e. RR x = ( y [,) z ) -> x e. dom vol ) )
14	2 13	mpd	|- ( x e. ran ( [,) |` ( RR X. RR ) ) -> x e. dom vol )
15	14	rgen	|- A. x e. ran ( [,) |` ( RR X. RR ) ) x e. dom vol
16		dfss3	|- ( ran ( [,) |` ( RR X. RR ) ) C_ dom vol <-> A. x e. ran ( [,) |` ( RR X. RR ) ) x e. dom vol )
17	15 16	mpbir	|- ran ( [,) |` ( RR X. RR ) ) C_ dom vol