uniioombl

Description: A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) Lemma 565Ca of Fremlin5 p. 214. (Contributed by Mario Carneiro, 26-Mar-2015)

	Ref	Expression
Hypotheses	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
Assertion	uniioombl	$⊢ φ \to ⋃ ran ((.) \circ F) \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
5		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
6		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	5 6	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
8		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
9	1 7 8	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
10		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
11	4 9 10	sylancr	$⊢ φ \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
12	11	frnd	$⊢ φ \to ran ((.) \circ F) \subseteq 𝒫 ℝ$
13		sspwuni	$⊢ ran ((.) \circ F) \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran ((.) \circ F) \subseteq ℝ$
14	12 13	sylib	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ℝ$
15		elpwi	$⊢ z \in 𝒫 ℝ \to z \subseteq ℝ$
16	15	ad2antrl	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \to z \subseteq ℝ$
17		simprr	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z) \in ℝ$
18		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
19	18	rphalfcld	$⊢ r \in ℝ^{+} \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
20		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
21	20	ovolgelb	$⊢ (z \subseteq ℝ \land {vol}^{} (z) \in ℝ \land \frac{\frac{r}{2}}{2} \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2}))$
22	16 17 19 21	syl2an3an	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2}))$
23	1	ad3antrrr	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
24	2	ad3antrrr	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to \underset{x \in ℕ}{Disj} (.) (F (x))$
25		eqid	$⊢ ⋃ ran ((.) \circ F) = ⋃ ran ((.) \circ F)$
26	17	adantr	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \to {vol}^{} (z) \in ℝ$
27	26	adantr	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (z) + (\frac{\frac{r}{2}}{2})))) \to {vol}^{} (z) \in ℝ$
28	18	adantl	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
29	28	adantr	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to \frac{r}{2} \in ℝ^{+}$
30	29	rphalfcld	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
31		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
32	31	ad2antrl	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
33		simprrl	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})))) \to z \subseteq ⋃ ran ((.) \circ f)$
34		simprrr	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (z) + (\frac{\frac{r}{2}}{2})))) \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (z) + (\frac{\frac{r}{2}}{2})$
35	23 24 3 25 27 30 32 33 20 34	uniioombllem6	$⊢ (((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (z \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (z) + (\frac{\frac{r}{2}}{2})))) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) + 4 (\frac{\frac{r}{2}}{2})$
36	22 35	rexlimddv	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) + 4 (\frac{\frac{r}{2}}{2})$
37		rpcn	$⊢ r \in ℝ^{+} \to r \in ℂ$
38	37	adantl	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to r \in ℂ$
39		2cnd	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 2 \in ℂ$
40		2ne0	$⊢ 2 \neq 0$
41	40	a1i	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 2 \neq 0$
42	38 39 39 41 41	divdiv1d	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to \frac{\frac{r}{2}}{2} = \frac{r}{2 \cdot 2}$
43		2t2e4	$⊢ 2 \cdot 2 = 4$
44	43	oveq2i	$⊢ \frac{r}{2 \cdot 2} = \frac{r}{4}$
45	42 44	eqtrdi	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to \frac{\frac{r}{2}}{2} = \frac{r}{4}$
46	45	oveq2d	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 4 (\frac{\frac{r}{2}}{2}) = 4 (\frac{r}{4})$
47		4cn	$⊢ 4 \in ℂ$
48	47	a1i	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 4 \in ℂ$
49		4ne0	$⊢ 4 \neq 0$
50	49	a1i	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 4 \neq 0$
51	38 48 50	divcan2d	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 4 (\frac{r}{4}) = r$
52	46 51	eqtrd	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \land r \in ℝ^{+}) \to 4 (\frac{\frac{r}{2}}{2}) = r$
53	52	oveq2d	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \to {vol}^{} (z) + 4 (\frac{\frac{r}{2}}{2}) = {vol}^{*} (z) + r$
54	36 53	breqtrd	$⊢ ((φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \land r \in ℝ^{+}) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) + r$
55	54	ralrimiva	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to \forall r \in ℝ^{+} {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) + r$
56		inss1	$⊢ z \cap ⋃ ran ((.) \circ F) \subseteq z$
57	56	a1i	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \to z \cap ⋃ ran ((.) \circ F) \subseteq z$
58		ovolsscl	$⊢ (z \cap ⋃ ran ((.) \circ F) \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) \in ℝ$
59	57 16 17 58	syl3anc	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) \in ℝ$
60		difssd	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{*} (z) \in ℝ)) \to z ∖ ⋃ ran ((.) \circ F) \subseteq z$
61		ovolsscl	$⊢ (z ∖ ⋃ ran ((.) \circ F) \subseteq z \land z \subseteq ℝ \land {vol}^{} (z) \in ℝ) \to {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \in ℝ$
62	60 16 17 61	syl3anc	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \in ℝ$
63	59 62	readdcld	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{*} (z ∖ ⋃ ran ((.) \circ F)) \in ℝ$
64		alrple	$⊢ ({vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \in ℝ \land {vol}^{} (z) \in ℝ) \to ({vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) \leftrightarrow \forall r \in ℝ^{+} {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{*} (z) + r)$
65	63 17 64	syl2anc	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to ({vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z) \leftrightarrow \forall r \in ℝ^{+} {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{*} (z) + r)$
66	55 65	mpbird	$⊢ (φ \land (z \in 𝒫 ℝ \land {vol}^{} (z) \in ℝ)) \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z)$
67	66	expr	$⊢ (φ \land z \in 𝒫 ℝ) \to ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z))$
68	67	ralrimiva	$⊢ φ \to \forall z \in 𝒫 ℝ ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z))$
69		ismbl2	$⊢ ⋃ ran ((.) \circ F) \in dom vol \leftrightarrow (⋃ ran ((.) \circ F) \subseteq ℝ \land \forall z \in 𝒫 ℝ ({vol}^{} (z) \in ℝ \to {vol}^{} (z \cap ⋃ ran ((.) \circ F)) + {vol}^{} (z ∖ ⋃ ran ((.) \circ F)) \leq {vol}^{} (z)))$
70	14 68 69	sylanbrc	$⊢ φ \to ⋃ ran ((.) \circ F) \in dom vol$

Metamath Proof Explorer

Theorem uniioombl

Proof