ioombl1

Description: An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

		Ref	Expression
	Assertion	ioombl1	$⊢ A \in ℝ^{*} \to (A, +∞) \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		ioossre	$⊢ (A, +∞) \subseteq ℝ$
3	2	a1i	$⊢ A \in ℝ \to (A, +∞) \subseteq ℝ$
4		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
5		simplrl	$⊢ ((A \in ℝ \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \land y \in ℝ^{+}) \to x \subseteq ℝ$
6		simplrr	$⊢ ((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \to {vol}^{} (x) \in ℝ$
7		simpr	$⊢ ((A \in ℝ \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
8		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
9	8	ovolgelb	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ \land y \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y)$
10	5 6 7 9	syl3anc	$⊢ ((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y)$
11		eqid	$⊢ (A, +∞) = (A, +∞)$
12		simplll	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to A \in ℝ$
13	5	adantr	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to x \subseteq ℝ$
14	6	adantr	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (x) + y))) \to {vol}^{} (x) \in ℝ$
15		simplr	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to y \in ℝ^{+}$
16		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m))), 2^{nd} (f (m))⟩))) = seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m))), 2^{nd} (f (m))⟩)))$
17		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)), if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m)))⟩))) = seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)), if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m)))⟩)))$
18		simprl	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to f \in ({(\leq \cap ℝ^{2})}^{ℕ})$
19		elovolmlem	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow f : ℕ ⟶ \leq \cap ℝ^{2}$
20	18 19	sylib	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
21		simprrl	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y))) \to x \subseteq ⋃ ran ((.) \circ f)$
22		simprrr	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (x) + y))) \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (x) + y$
23		eqid	$⊢ 1^{st} (f (n)) = 1^{st} (f (n))$
24		eqid	$⊢ 2^{nd} (f (n)) = 2^{nd} (f (n))$
25		2fveq3	$⊢ m = n \to 1^{st} (f (m)) = 1^{st} (f (n))$
26	25	breq1d	$⊢ m = n \to (1^{st} (f (m)) \leq A \leftrightarrow 1^{st} (f (n)) \leq A)$
27	26 25	ifbieq2d	$⊢ m = n \to if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) = if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n)))$
28		2fveq3	$⊢ m = n \to 2^{nd} (f (m)) = 2^{nd} (f (n))$
29	27 28	breq12d	$⊢ m = n \to (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)) \leftrightarrow if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)))$
30	29 27 28	ifbieq12d	$⊢ m = n \to if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m))) = if (if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)), if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))), 2^{nd} (f (n)))$
31	30 28	opeq12d	$⊢ m = n \to ⟨if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m))), 2^{nd} (f (m))⟩ = ⟨if (if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)), if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))), 2^{nd} (f (n))), 2^{nd} (f (n))⟩$
32	31	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m))), 2^{nd} (f (m))⟩) = (n \in ℕ ⟼ ⟨if (if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)), if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))), 2^{nd} (f (n))), 2^{nd} (f (n))⟩)$
33	25 30	opeq12d	$⊢ m = n \to ⟨1^{st} (f (m)), if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m)))⟩ = ⟨1^{st} (f (n)), if (if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)), if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))), 2^{nd} (f (n)))⟩$
34	33	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨1^{st} (f (m)), if (if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))) \leq 2^{nd} (f (m)), if (1^{st} (f (m)) \leq A, A, 1^{st} (f (m))), 2^{nd} (f (m)))⟩) = (n \in ℕ ⟼ ⟨1^{st} (f (n)), if (if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))) \leq 2^{nd} (f (n)), if (1^{st} (f (n)) \leq A, A, 1^{st} (f (n))), 2^{nd} (f (n)))⟩)$
35	11 12 13 14 15 8 16 17 20 21 22 23 24 32 34	ioombl1lem4	$⊢ (((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (x \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (x) + y))) \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x) + y$
36	10 35	rexlimddv	$⊢ ((A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \land y \in ℝ^{+}) \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x) + y$
37	36	ralrimiva	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to \forall y \in ℝ^{+} {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x) + y$
38		inss1	$⊢ x \cap (A, +∞) \subseteq x$
39		ovolsscl	$⊢ (x \cap (A, +∞) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (A, +∞)) \in ℝ$
40	38 39	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (A, +∞)) \in ℝ$
41	40	adantl	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A, +∞)) \in ℝ$
42		difss	$⊢ x ∖ (A, +∞) \subseteq x$
43		ovolsscl	$⊢ (x ∖ (A, +∞) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ (A, +∞)) \in ℝ$
44	42 43	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ (A, +∞)) \in ℝ$
45	44	adantl	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ (A, +∞)) \in ℝ$
46	41 45	readdcld	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A, +∞)) + {vol}^{*} (x ∖ (A, +∞)) \in ℝ$
47		simprr	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x) \in ℝ$
48		alrple	$⊢ ({vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \in ℝ \land {vol}^{} (x) \in ℝ) \to ({vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x) \leftrightarrow \forall y \in ℝ^{+} {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{*} (x) + y)$
49	46 47 48	syl2anc	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to ({vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x) \leftrightarrow \forall y \in ℝ^{+} {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{*} (x) + y)$
50	37 49	mpbird	$⊢ (A \in ℝ \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x)$
51	50	expr	$⊢ (A \in ℝ \land x \subseteq ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x))$
52	4 51	sylan2	$⊢ (A \in ℝ \land x \in 𝒫 ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x))$
53	52	ralrimiva	$⊢ A \in ℝ \to \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x))$
54		ismbl2	$⊢ (A, +∞) \in dom vol \leftrightarrow ((A, +∞) \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A, +∞)) + {vol}^{} (x ∖ (A, +∞)) \leq {vol}^{} (x)))$
55	3 53 54	sylanbrc	$⊢ A \in ℝ \to (A, +∞) \in dom vol$
56		oveq1	$⊢ A = +∞ \to (A, +∞) = (+∞, +∞)$
57		iooid	$⊢ (+∞, +∞) = \emptyset$
58	56 57	eqtrdi	$⊢ A = +∞ \to (A, +∞) = \emptyset$
59		0mbl	$⊢ \emptyset \in dom vol$
60	58 59	eqeltrdi	$⊢ A = +∞ \to (A, +∞) \in dom vol$
61		oveq1	$⊢ A = −∞ \to (A, +∞) = (−∞, +∞)$
62		ioomax	$⊢ (−∞, +∞) = ℝ$
63	61 62	eqtrdi	$⊢ A = −∞ \to (A, +∞) = ℝ$
64		rembl	$⊢ ℝ \in dom vol$
65	63 64	eqeltrdi	$⊢ A = −∞ \to (A, +∞) \in dom vol$
66	55 60 65	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to (A, +∞) \in dom vol$
67	1 66	sylbi	$⊢ A \in ℝ^{*} \to (A, +∞) \in dom vol$

Metamath Proof Explorer

Theorem ioombl1

Proof