Theorem uniioombllem1

Description: Lemma for uniioombl . (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)$$
	uniioombl.a	$$⊢A=\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)$$
	uniioombl.e	$$⊢\phi \to {vol}^{*}\left(E\right)\in ℝ$$
	uniioombl.c	$$⊢\phi \to C\in {ℝ}^{+}$$
	uniioombl.g	$$⊢\phi \to G:\mathbb{N}⟶\le \cap {ℝ}^2$$
	uniioombl.s	$$⊢\phi \to E\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ G\right)$$
	uniioombl.t	$$⊢T=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ G\right)\right)$$
	uniioombl.v	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\le {vol}^{*}\left(E\right)+C$$
Assertion	uniioombllem1	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\in ℝ$$

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		uniioombl.a	$$⊢A=\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)$$
5		uniioombl.e	$$⊢\phi \to {vol}^{*}\left(E\right)\in ℝ$$
6		uniioombl.c	$$⊢\phi \to C\in {ℝ}^{+}$$
7		uniioombl.g	$$⊢\phi \to G:\mathbb{N}⟶\le \cap {ℝ}^2$$
8		uniioombl.s	$$⊢\phi \to E\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ G\right)$$
9		uniioombl.t	$$⊢T=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ G\right)\right)$$
10		uniioombl.v	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\le {vol}^{*}\left(E\right)+C$$
11		eqid	$$⊢\left(\mathrm{abs}\circ -\right)\circ G=\left(\mathrm{abs}\circ -\right)\circ G$$
12	11 9	ovolsf	$$⊢G:\mathbb{N}⟶\le \cap {ℝ}^2\to T:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
13	7 12	syl	$$⊢\phi \to T:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
14	13	frnd	$$⊢\phi \to \mathrm{ran}T\subseteq \left[0,\mathrm{+\infty }\right)$$
15		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
16	14 15	sstrdi	$$⊢\phi \to \mathrm{ran}T\subseteq ℝ$$
17		1nn	$$⊢1\in \mathbb{N}$$
18	13	fdmd	$$⊢\phi \to \mathrm{dom}T=\mathbb{N}$$
19	17 18	eleqtrrid	$$⊢\phi \to 1\in \mathrm{dom}T$$
20	19	ne0d	$$⊢\phi \to \mathrm{dom}T\ne \varnothing$$
21		dm0rn0	$$⊢\mathrm{dom}T=\varnothing \leftrightarrow \mathrm{ran}T=\varnothing$$
22	21	necon3bii	$$⊢\mathrm{dom}T\ne \varnothing \leftrightarrow \mathrm{ran}T\ne \varnothing$$
23	20 22	sylib	$$⊢\phi \to \mathrm{ran}T\ne \varnothing$$
24		icossxr	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$$
25	14 24	sstrdi	$$⊢\phi \to \mathrm{ran}T\subseteq {ℝ}^{*}$$
26		supxrcl	$$⊢\mathrm{ran}T\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
27	25 26	syl	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
28	6	rpred	$$⊢\phi \to C\in ℝ$$
29	5 28	readdcld	$$⊢\phi \to {vol}^{*}\left(E\right)+C\in ℝ$$
30	29	rexrd	$$⊢\phi \to {vol}^{*}\left(E\right)+C\in {ℝ}^{*}$$
31		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
32	31	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
33	29	ltpnfd	$$⊢\phi \to {vol}^{*}\left(E\right)+C<\mathrm{+\infty }$$
34	27 30 32 10 33	xrlelttrd	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)<\mathrm{+\infty }$$
35		supxrbnd	$$⊢\left(\mathrm{ran}T\subseteq ℝ\wedge \mathrm{ran}T\ne \varnothing \wedge sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)<\mathrm{+\infty }\right)\to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\in ℝ$$
36	16 23 34 35	syl3anc	$$⊢\phi \to sup\left(\mathrm{ran}T,{ℝ}^{*},<\right)\in ℝ$$