icombl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > icombl		Structured version Visualization version GIF version

Theorem icombl 25878

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

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

**Proof of Theorem icombl**
Step	Hyp	Ref	Expression
1		uncom 4105	. . . . 5 ⊢ ((𝐵[,)+∞) ∪ (𝐴[,)𝐵)) = ((𝐴[,)𝐵) ∪ (𝐵[,)+∞))
2		rexr 11348	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
3	2	ad2antrr 739	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ^)
4		simplr 781	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ^)
5		pnfxr 11356	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 < 𝐵) → +∞ ∈ ℝ^)
7		xrltle 13271	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
8	2, 7	sylan 592	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
9	8	imp 412	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵)
10		pnfge 13252	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ +∞)
11	4, 10	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐵 ≤ +∞)
12		icoun 13599	. . . . . 6 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ +∞)) → ((𝐴[,)𝐵) ∪ (𝐵[,)+∞)) = (𝐴[,)+∞))
13	3, 4, 6, 9, 11, 12	syl32anc 1405	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐴[,)𝐵) ∪ (𝐵[,)+∞)) = (𝐴[,)+∞))
14	1, 13	eqtrid 2808	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∪ (𝐴[,)𝐵)) = (𝐴[,)+∞))
15		ssun1 4124	. . . . . 6 ⊢ (𝐵[,)+∞) ⊆ ((𝐵[,)+∞) ∪ (𝐴[,)𝐵))
16	15, 14	sseqtrid 3973	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ⊆ (𝐴[,)+∞))
17		incom 4155	. . . . . 6 ⊢ ((𝐵[,)+∞) ∩ (𝐴[,)𝐵)) = ((𝐴[,)𝐵) ∩ (𝐵[,)+∞))
18		icodisj 13600	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐴[,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
19	5, 18	mp3an3 1479	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
20	3, 4, 19	syl2anc 596	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐴[,)𝐵) ∩ (𝐵[,)+∞)) = ∅)
21	17, 20	eqtrid 2808	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵[,)+∞) ∩ (𝐴[,)𝐵)) = ∅)
22		uneqdifeq 4448	. . . . 5 ⊢ (((𝐵[,)+∞) ⊆ (𝐴[,)+∞) ∧ ((𝐵[,)+∞) ∩ (𝐴[,)𝐵)) = ∅) → (((𝐵[,)+∞) ∪ (𝐴[,)𝐵)) = (𝐴[,)+∞) ↔ ((𝐴[,)+∞) ∖ (𝐵[,)+∞)) = (𝐴[,)𝐵)))
23	16, 21, 22	syl2anc 596	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (((𝐵[,)+∞) ∪ (𝐴[,)𝐵)) = (𝐴[,)+∞) ↔ ((𝐴[,)+∞) ∖ (𝐵[,)+∞)) = (𝐴[,)𝐵)))
24	14, 23	mpbid 235	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐴[,)+∞) ∖ (𝐵[,)+∞)) = (𝐴[,)𝐵))
25		icombl1 25877	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol)
26	25	ad2antrr 739	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐴[,)+∞) ∈ dom vol)
27		xrleloe 13266	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
28	4, 6, 27	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 ≤ +∞ ↔ (𝐵 < +∞ ∨ 𝐵 = +∞)))
29	11, 28	mpbid 235	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ ∨ 𝐵 = +∞))
30		simpr 490	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
31		xrre2 13293	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < +∞)) → 𝐵 ∈ ℝ)
32	31	expr 462	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
33	3, 4, 6, 30, 32	syl31anc 1400	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 < +∞ → 𝐵 ∈ ℝ))
34	33	orim1d 981	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐵 < +∞ ∨ 𝐵 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)))
35	29, 34	mpd 16	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞))
36		icombl1 25877	. . . . . 6 ⊢ (𝐵 ∈ ℝ → (𝐵[,)+∞) ∈ dom vol)
37		oveq1 7425	. . . . . . . 8 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) = (+∞[,)+∞))
38		pnfge 13252	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → +∞ ≤ +∞)
39	5, 38	ax-mp 5	. . . . . . . . 9 ⊢ +∞ ≤ +∞
40		ico0 13515	. . . . . . . . . 10 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞))
41	5, 5, 40	mp2an 705	. . . . . . . . 9 ⊢ ((+∞[,)+∞) = ∅ ↔ +∞ ≤ +∞)
42	39, 41	mpbir 234	. . . . . . . 8 ⊢ (+∞[,)+∞) = ∅
43	37, 42	eqtrdi 2812	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) = ∅)
44		0mbl 25853	. . . . . . 7 ⊢ ∅ ∈ dom vol
45	43, 44	eqeltrdi 2869	. . . . . 6 ⊢ (𝐵 = +∞ → (𝐵[,)+∞) ∈ dom vol)
46	36, 45	jaoi 871	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∨ 𝐵 = +∞) → (𝐵[,)+∞) ∈ dom vol)
47	35, 46	syl 18	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐵[,)+∞) ∈ dom vol)
48		difmbl 25857	. . . 4 ⊢ (((𝐴[,)+∞) ∈ dom vol ∧ (𝐵[,)+∞) ∈ dom vol) → ((𝐴[,)+∞) ∖ (𝐵[,)+∞)) ∈ dom vol)
49	26, 47, 48	syl2anc 596	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → ((𝐴[,)+∞) ∖ (𝐵[,)+∞)) ∈ dom vol)
50	24, 49	eqeltrrd 2862	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 < 𝐵) → (𝐴[,)𝐵) ∈ dom vol)
51		ico0 13515	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
52	2, 51	sylan 592	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
53		simpr 490	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → 𝐵 ∈ ℝ^)
54	2	adantr 486	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → 𝐴 ∈ ℝ^)
55	53, 54	xrlenltd 11368	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
56	52, 55	bitrd 282	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → ((𝐴[,)𝐵) = ∅ ↔ ¬ 𝐴 < 𝐵))
57	56	biimpar 483	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐴 < 𝐵) → (𝐴[,)𝐵) = ∅)
58	57, 44	eqeltrdi 2869	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ ¬ 𝐴 < 𝐵) → (𝐴[,)𝐵) ∈ dom vol)
59	50, 58	pm2.61dan 825	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴[,)𝐵) ∈ dom vol)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 class class class wbr 5103 dom cdm 5651 (class class class)co 7418 ℝcr 11192 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 [,)cico 13471 volcvol 25777

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-z 12687 df-uz 12959 df-q 13069 df-rp 13114 df-xadd 13235 df-ioo 13473 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-rlim 15649 df-sum 15847 df-xmet 21664 df-met 21665 df-ovol 25778 df-vol 25779

This theorem is used by: ioombl 25879 volicoff 46974 voliooicof 46975 icoresmbl 47522 hoiprodcl 47526 hoiprodcl3 47559 hoidmvcl 47561 hsphoidmvle2 47564 hsphoidmvle 47565 hoidmv1lelem1 47570 hoidmv1lelem2 47571 hoidmv1lelem3 47572 hoidifhspdmvle 47599 volicorege0 47616 ovolval5lem1 47631

W3C validator