ioombl

Description: An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014)

		Ref	Expression
	Assertion	ioombl	$⊢ (A, B) \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		snunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \{A\} \cup (A, B) = [A, B)$
2	1	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to \{A\} \cup (A, B) = [A, B)$
3	2	adantrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to \{A\} \cup (A, B) = [A, B)$
4		lbico1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \in [A, B)$
5	4	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to A \in [A, B)$
6	5	adantrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to A \in [A, B)$
7	6	snssd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to \{A\} \subseteq [A, B)$
8		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
9	8	ad2antrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, A] = \{A\}$
10	9	ineq1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, A] \cap (A, B) = \{A\} \cap (A, B)$
11		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to A \in ℝ^{*}$
12		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to B \in ℝ^{*}$
13		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
14		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
15		xrltnle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \leftrightarrow \neg w \leq A)$
16	13 14 15	ixxdisj	$⊢ (A \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \to [A, A] \cap (A, B) = \emptyset$
17	11 11 12 16	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, A] \cap (A, B) = \emptyset$
18	10 17	eqtr3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to \{A\} \cap (A, B) = \emptyset$
19		uneqdifeq	$⊢ (\{A\} \subseteq [A, B) \land \{A\} \cap (A, B) = \emptyset) \to (\{A\} \cup (A, B) = [A, B) \leftrightarrow [A, B) ∖ \{A\} = (A, B))$
20	7 18 19	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to (\{A\} \cup (A, B) = [A, B) \leftrightarrow [A, B) ∖ \{A\} = (A, B))$
21	3 20	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, B) ∖ \{A\} = (A, B)$
22		mnfxr	$⊢ −∞ \in ℝ^{*}$
23	22	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to −∞ \in ℝ^{*}$
24		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to −∞ < A$
25		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to A < B$
26		xrre2	$⊢ ((−∞ \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \land (−∞ < A \land A < B)) \to A \in ℝ$
27	23 11 12 24 25 26	syl32anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to A \in ℝ$
28		icombl	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \in dom vol$
29	27 12 28	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, B) \in dom vol$
30	27	snssd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to \{A\} \subseteq ℝ$
31		ovolsn	$⊢ A \in ℝ \to {vol}^{*} (\{A\}) = 0$
32	27 31	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to {vol}^{*} (\{A\}) = 0$
33		nulmbl	$⊢ (\{A\} \subseteq ℝ \land {vol}^{*} (\{A\}) = 0) \to \{A\} \in dom vol$
34	30 32 33	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to \{A\} \in dom vol$
35		difmbl	$⊢ ([A, B) \in dom vol \land \{A\} \in dom vol) \to [A, B) ∖ \{A\} \in dom vol$
36	29 34 35	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to [A, B) ∖ \{A\} \in dom vol$
37	21 36	eqeltrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < B \land −∞ < A)) \to (A, B) \in dom vol$
38	37	expr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞ < A \to (A, B) \in dom vol)$
39		uncom	$⊢ [B, +∞) \cup (−∞, B) = (−∞, B) \cup [B, +∞)$
40	22	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to −∞ \in ℝ^{*}$
41		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to B \in ℝ^{*}$
42		pnfxr	$⊢ +∞ \in ℝ^{*}$
43	42	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to +∞ \in ℝ^{*}$
44		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to A \in ℝ^{*}$
45		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
46	45	ad2antrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to −∞ \leq A$
47		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to A < B$
48	40 44 41 46 47	xrlelttrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to −∞ < B$
49		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
50	41 49	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to B \leq +∞$
51		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
52		xrlenlt	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B \leq w \leftrightarrow \neg w < B)$
53		xrltletr	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((w < B \land B \leq +∞) \to w < +∞)$
54		xrltletr	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((−∞ < B \land B \leq w) \to −∞ < w)$
55	14 51 52 14 53 54	ixxun	$⊢ ((−∞ \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \land (−∞ < B \land B \leq +∞)) \to (−∞, B) \cup [B, +∞) = (−∞, +∞)$
56	40 41 43 48 50 55	syl32anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞, B) \cup [B, +∞) = (−∞, +∞)$
57	39 56	eqtrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to [B, +∞) \cup (−∞, B) = (−∞, +∞)$
58		ioomax	$⊢ (−∞, +∞) = ℝ$
59	57 58	eqtrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to [B, +∞) \cup (−∞, B) = ℝ$
60		ssun1	$⊢ [B, +∞) \subseteq [B, +∞) \cup (−∞, B)$
61	60 59	sseqtrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to [B, +∞) \subseteq ℝ$
62		incom	$⊢ [B, +∞) \cap (−∞, B) = (−∞, B) \cap [B, +∞)$
63	14 51 52	ixxdisj	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \to (−∞, B) \cap [B, +∞) = \emptyset$
64	40 41 43 63	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞, B) \cap [B, +∞) = \emptyset$
65	62 64	eqtrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to [B, +∞) \cap (−∞, B) = \emptyset$
66		uneqdifeq	$⊢ ([B, +∞) \subseteq ℝ \land [B, +∞) \cap (−∞, B) = \emptyset) \to ([B, +∞) \cup (−∞, B) = ℝ \leftrightarrow ℝ ∖ [B, +∞) = (−∞, B))$
67	61 65 66	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to ([B, +∞) \cup (−∞, B) = ℝ \leftrightarrow ℝ ∖ [B, +∞) = (−∞, B))$
68	59 67	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to ℝ ∖ [B, +∞) = (−∞, B)$
69		rembl	$⊢ ℝ \in dom vol$
70		xrleloe	$⊢ (B \in ℝ^{} \land +∞ \in ℝ^{}) \to (B \leq +∞ \leftrightarrow (B < +∞ \lor B = +∞))$
71	41 42 70	sylancl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (B \leq +∞ \leftrightarrow (B < +∞ \lor B = +∞))$
72	50 71	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (B < +∞ \lor B = +∞)$
73		xrre2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \land (A < B \land B < +∞)) \to B \in ℝ$
74	73	expr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \land A < B) \to (B < +∞ \to B \in ℝ)$
75	42 74	mp3anl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (B < +∞ \to B \in ℝ)$
76	75	orim1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to ((B < +∞ \lor B = +∞) \to (B \in ℝ \lor B = +∞))$
77	72 76	mpd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (B \in ℝ \lor B = +∞)$
78		icombl1	$⊢ B \in ℝ \to [B, +∞) \in dom vol$
79		oveq1	$⊢ B = +∞ \to [B, +∞) = [+∞, +∞)$
80		pnfge	$⊢ +∞ \in ℝ^{*} \to +∞ \leq +∞$
81	42 80	ax-mp	$⊢ +∞ \leq +∞$
82		ico0	$⊢ (+∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to ([+∞, +∞) = \emptyset \leftrightarrow +∞ \leq +∞)$
83	42 42 82	mp2an	$⊢ [+∞, +∞) = \emptyset \leftrightarrow +∞ \leq +∞$
84	81 83	mpbir	$⊢ [+∞, +∞) = \emptyset$
85	79 84	eqtrdi	$⊢ B = +∞ \to [B, +∞) = \emptyset$
86		0mbl	$⊢ \emptyset \in dom vol$
87	85 86	eqeltrdi	$⊢ B = +∞ \to [B, +∞) \in dom vol$
88	78 87	jaoi	$⊢ (B \in ℝ \lor B = +∞) \to [B, +∞) \in dom vol$
89	77 88	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to [B, +∞) \in dom vol$
90		difmbl	$⊢ (ℝ \in dom vol \land [B, +∞) \in dom vol) \to ℝ ∖ [B, +∞) \in dom vol$
91	69 89 90	sylancr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to ℝ ∖ [B, +∞) \in dom vol$
92	68 91	eqeltrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞, B) \in dom vol$
93		oveq1	$⊢ −∞ = A \to (−∞, B) = (A, B)$
94	93	eleq1d	$⊢ −∞ = A \to ((−∞, B) \in dom vol \leftrightarrow (A, B) \in dom vol)$
95	92 94	syl5ibcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞ = A \to (A, B) \in dom vol)$
96		xrleloe	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (−∞ \leq A \leftrightarrow (−∞ < A \lor −∞ = A))$
97	22 44 96	sylancr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞ \leq A \leftrightarrow (−∞ < A \lor −∞ = A))$
98	46 97	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (−∞ < A \lor −∞ = A)$
99	38 95 98	mpjaod	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A < B) \to (A, B) \in dom vol$
100		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
101		xrlenlt	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
102	101	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \leq A \leftrightarrow \neg A < B)$
103	100 102	bitrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow \neg A < B)$
104	103	biimpar	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A < B) \to (A, B) = \emptyset$
105	104 86	eqeltrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg A < B) \to (A, B) \in dom vol$
106	99 105	pm2.61dan	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) \in dom vol$
107		ndmioo	$⊢ \neg (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \emptyset$
108	107 86	eqeltrdi	$⊢ \neg (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) \in dom vol$
109	106 108	pm2.61i	$⊢ (A, B) \in dom vol$

Metamath Proof Explorer

Theorem ioombl

Proof