Theorem icombl

Description: A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

	Ref	Expression
Assertion	icombl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) )
2		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
3	2	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
4		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6	5	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → +∞ ∈ ℝ* )
7		xrltle	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
8	2 7	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
9	8	imp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
10		pnfge	⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
11	4 10	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐵 ≤ +∞ )
12		icoun	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ +∞ ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
13	3 4 6 9 11 12	syl32anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) +∞ ) )
14	1 13	syl5eq	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) )
15		ssun1	⊢ ( 𝐵 [,) +∞ ) ⊆ ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) )
16	15 14	sseqtrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) )
17		incom	⊢ ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) )
18		icodisj	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
19	5 18	mp3an3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
20	3 4 19	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) +∞ ) ) = ∅ )
21	17 20	syl5eq	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ∅ )
22		uneqdifeq	⊢ ( ( ( 𝐵 [,) +∞ ) ⊆ ( 𝐴 [,) +∞ ) ∧ ( ( 𝐵 [,) +∞ ) ∩ ( 𝐴 [,) 𝐵 ) ) = ∅ ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) ↔ ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) ) )
23	16 21 22	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 [,) +∞ ) ∪ ( 𝐴 [,) 𝐵 ) ) = ( 𝐴 [,) +∞ ) ↔ ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) ) )
24	14 23	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) = ( 𝐴 [,) 𝐵 ) )
25		icombl1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ dom vol )
26	25	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,) +∞ ) ∈ dom vol )
27		xrleloe	⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
28	4 6 27	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ≤ +∞ ↔ ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) ) )
29	11 28	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) )
30		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
31		xrre2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < +∞ ) ) → 𝐵 ∈ ℝ )
32	31	expr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
33	3 4 6 30 32	syl31anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 < +∞ → 𝐵 ∈ ℝ ) )
34	33	orim1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 < +∞ ∨ 𝐵 = +∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) )
35	29 34	mpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
36		icombl1	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 [,) +∞ ) ∈ dom vol )
37		oveq1	⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ( +∞ [,) +∞ ) )
38		pnfge	⊢ ( +∞ ∈ ℝ* → +∞ ≤ +∞ )
39	5 38	ax-mp	⊢ +∞ ≤ +∞
40		ico0	⊢ ( ( +∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ ) )
41	5 5 40	mp2an	⊢ ( ( +∞ [,) +∞ ) = ∅ ↔ +∞ ≤ +∞ )
42	39 41	mpbir	⊢ ( +∞ [,) +∞ ) = ∅
43	37 42	eqtrdi	⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) = ∅ )
44		0mbl	⊢ ∅ ∈ dom vol
45	43 44	eqeltrdi	⊢ ( 𝐵 = +∞ → ( 𝐵 [,) +∞ ) ∈ dom vol )
46	36 45	jaoi	⊢ ( ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
47	35 46	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 [,) +∞ ) ∈ dom vol )
48		difmbl	⊢ ( ( ( 𝐴 [,) +∞ ) ∈ dom vol ∧ ( 𝐵 [,) +∞ ) ∈ dom vol ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
49	26 47 48	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 [,) +∞ ) ∖ ( 𝐵 [,) +∞ ) ) ∈ dom vol )
50	24 49	eqeltrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
51		ico0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
52	2 51	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
53		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ℝ* )
54	2	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
55	53 54	xrlenltd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
56	52 55	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ ¬ 𝐴 < 𝐵 ) )
57	56	biimpar	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) = ∅ )
58	57 44	eqeltrdi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
59	50 58	pm2.61dan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )