# Metamath Proof Explorer

## Theorem uniioombllem1

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{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}:ℕ⟶\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}:ℕ⟶\le \cap {ℝ}^{2}$
2 uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{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}:ℕ⟶\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}:ℕ⟶\le \cap {ℝ}^{2}\to {T}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
13 7 12 syl ${⊢}{\phi }\to {T}:ℕ⟶\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 ℕ$
18 13 fdmd ${⊢}{\phi }\to \mathrm{dom}{T}=ℕ$
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 ↔\mathrm{ran}{T}=\varnothing$
22 21 necon3bii ${⊢}\mathrm{dom}{T}\ne \varnothing ↔\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 ℝ$