Theorem uniiccmbl

Description: An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) (Contributed by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Hypotheses	uniioombl.1	$$⊢\phi \to F:\mathbb{N}⟶\le \cap {ℝ}^2$$
	uniioombl.2	$$⊢\phi \to \underset{x\in \mathbb{N}}{Disj}\left(.\right)\left(F\left(x\right)\right)$$
	uniioombl.3	$$⊢S=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\right)$$
Assertion	uniiccmbl	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$$⊢\phi \to F:\mathbb{N}⟶\le \cap {ℝ}^2$$
2		uniioombl.2	$$⊢\phi \to \underset{x\in \mathbb{N}}{Disj}\left(.\right)\left(F\left(x\right)\right)$$
3		uniioombl.3	$$⊢S=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\right)$$
4	1	uniiccdif	$$⊢\phi \to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)=0\right)$$
5	4	simpld	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)$$
6		undif	$$⊢\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\leftrightarrow \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\cup \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)=\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)$$
7	5 6	sylib	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\cup \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)=\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)$$
8	1 2 3	uniioombl	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\in \mathrm{dom}vol$$
9		ovolficcss	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\subseteq ℝ$$
10	1 9	syl	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\subseteq ℝ$$
11	10	ssdifssd	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\subseteq ℝ$$
12	4	simprd	$$⊢\phi \to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)=0$$
13		nulmbl	$$⊢\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)=0\right)\to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\in \mathrm{dom}vol$$
14	11 12 13	syl2anc	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\in \mathrm{dom}vol$$
15		unmbl	$$⊢\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\in \mathrm{dom}vol\wedge \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\in \mathrm{dom}vol\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\cup \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)\in \mathrm{dom}vol$$
16	8 14 15	syl2anc	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\cup \left(\bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)\right)\in \mathrm{dom}vol$$
17	7 16	eqeltrrd	$$⊢\phi \to \bigcup \mathrm{ran}\left(\left[.\right]\circ F\right)\in \mathrm{dom}vol$$