Theorem uniioombllem1

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

	Ref	Expression
Hypotheses	uniioombl.1	|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
	uniioombl.2	|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
	uniioombl.3	|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
	uniioombl.a	|- A = U. ran ( (,) o. F )
	uniioombl.e	|- ( ph -> ( vol* ` E ) e. RR )
	uniioombl.c	|- ( ph -> C e. RR+ )
	uniioombl.g	|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
	uniioombl.s	|- ( ph -> E C_ U. ran ( (,) o. G ) )
	uniioombl.t	|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
	uniioombl.v	|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
Assertion	uniioombllem1	|- ( ph -> sup ( ran T , RR* , < ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2		uniioombl.2	|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
3		uniioombl.3	|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
4		uniioombl.a	|- A = U. ran ( (,) o. F )
5		uniioombl.e	|- ( ph -> ( vol* ` E ) e. RR )
6		uniioombl.c	|- ( ph -> C e. RR+ )
7		uniioombl.g	|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8		uniioombl.s	|- ( ph -> E C_ U. ran ( (,) o. G ) )
9		uniioombl.t	|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
10		uniioombl.v	|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
11		eqid	|- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
12	11 9	ovolsf	|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
13	7 12	syl	|- ( ph -> T : NN --> ( 0 [,) +oo ) )
14	13	frnd	|- ( ph -> ran T C_ ( 0 [,) +oo ) )
15		rge0ssre	|- ( 0 [,) +oo ) C_ RR
16	14 15	sstrdi	|- ( ph -> ran T C_ RR )
17		1nn	|- 1 e. NN
18	13	fdmd	|- ( ph -> dom T = NN )
19	17 18	eleqtrrid	|- ( ph -> 1 e. dom T )
20	19	ne0d	|- ( ph -> dom T =/= (/) )
21		dm0rn0	|- ( dom T = (/) <-> ran T = (/) )
22	21	necon3bii	|- ( dom T =/= (/) <-> ran T =/= (/) )
23	20 22	sylib	|- ( ph -> ran T =/= (/) )
24		icossxr	|- ( 0 [,) +oo ) C_ RR*
25	14 24	sstrdi	|- ( ph -> ran T C_ RR* )
26		supxrcl	|- ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* )
27	25 26	syl	|- ( ph -> sup ( ran T , RR* , < ) e. RR* )
28	6	rpred	|- ( ph -> C e. RR )
29	5 28	readdcld	|- ( ph -> ( ( vol* ` E ) + C ) e. RR )
30	29	rexrd	|- ( ph -> ( ( vol* ` E ) + C ) e. RR* )
31		pnfxr	|- +oo e. RR*
32	31	a1i	|- ( ph -> +oo e. RR* )
33	29	ltpnfd	|- ( ph -> ( ( vol* ` E ) + C ) < +oo )
34	27 30 32 10 33	xrlelttrd	|- ( ph -> sup ( ran T , RR* , < ) < +oo )
35		supxrbnd	|- ( ( ran T C_ RR /\ ran T =/= (/) /\ sup ( ran T , RR* , < ) < +oo ) -> sup ( ran T , RR* , < ) e. RR )
36	16 23 34 35	syl3anc	|- ( ph -> sup ( ran T , RR* , < ) e. RR )