Theorem omssubadd 28961

Description: A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.)

Hypotheses

Ref	Expression
oms.m	|- M = (toOMeas ` R )
oms.o	|- ( ph -> Q e. V )
oms.r	|- ( ph -> R : Q --> ( 0 [,] +oo ) )
omssubadd.a	|- ( ( ph /\ y e. X ) -> A C_ U. Q )
omssubadd.b	|- ( ph -> X ~<_ om )

Assertion

Ref	Expression
omssubadd	|- ( ph -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )

Distinct variable groups:   y, Q   y, R   y, V   ph, y   y, X

Allowed substitution hints:   A( y)   M( y)

Proof of Theorem omssubadd

Dummy variables x z e t u w f g c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omssubadd.b	. . . . . 6 |- ( ph -> X ~<_ om )
2		nnenom 12190	. . . . . . 7 |- NN ~~ om
3	2	ensymi 7626	. . . . . 6 |- om ~~ NN
4		domentr 7635	. . . . . 6 |- ( ( X ~<_ om /\ om ~~ NN ) -> X ~<_ NN )
5	1, 3, 4	sylancl 666	. . . . 5 |- ( ph -> X ~<_ NN )
6		brdomi 7588	. . . . 5 |- ( X ~<_ NN -> E. f f : X -1-1-> NN )
7	5, 6	syl 17	. . . 4 |- ( ph -> E. f f : X -1-1-> NN )
8	7	adantr 466	. . 3 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> E. f f : X -1-1-> NN )
9		simplll 766	. . . . . . . . . 10 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ph )
10		ctex 28135	. . . . . . . . . . 11 |- ( X ~<_ om -> X e. _V )
11	1, 10	syl 17	. . . . . . . . . 10 |- ( ph -> X e. _V )
12	9, 11	syl 17	. . . . . . . . 9 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> X e. _V )
13		nfv 1754	. . . . . . . . . . . . 13 |- F/ y ph
14		nfcv 2591	. . . . . . . . . . . . . . 15 |- F/_ y X
15	14	nfesum1 28700	. . . . . . . . . . . . . 14 |- F/_ yΣ* y e. X ( M ` A )
16		nfcv 2591	. . . . . . . . . . . . . 14 |- F/_ y RR
17	15, 16	nfel 2604	. . . . . . . . . . . . 13 |- F/ yΣ* y e. X ( M ` A ) e. RR
18	13, 17	nfan 1986	. . . . . . . . . . . 12 |- F/ y ( ph /\ Σ* y e. X ( M ` A ) e. RR )
19		nfv 1754	. . . . . . . . . . . 12 |- F/ y f : X -1-1-> NN
20	18, 19	nfan 1986	. . . . . . . . . . 11 |- F/ y ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
21		nfv 1754	. . . . . . . . . . 11 |- F/ y e e. RR+
22	20, 21	nfan 1986	. . . . . . . . . 10 |- F/ y ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
23	9	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
24		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> y e. X )
25	11	adantr 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> X e. _V )
26		oms.o	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> Q e. V )
27		oms.r	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> R : Q --> ( 0 [,] +oo ) )
28		omsf 28957	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
29		oms.m	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- M = (toOMeas ` R )
30	29	feq1i 5738	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
31	28, 30	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
32	26, 27, 31	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
33	32	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. X ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
34		omssubadd.a	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A C_ U. Q )
35		fdm 5750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
36	27, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> dom R = Q )
37	36	unieqd 4232	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> U. dom R = U. Q )
38	37	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> U. dom R = U. Q )
39	34, 38	sseqtr4d 3507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. X ) -> A C_ U. dom R )
40		uniexg 6602	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( Q e. V -> U. Q e. _V )
41	26, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> U. Q e. _V )
42	41	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. X ) -> U. Q e. _V )
43		ssexg 4571	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
44	34, 42, 43	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A e. _V )
45		elpwg 3993	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. _V -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. X ) -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
47	39, 46	mpbird 235	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. X ) -> A e. ~P U. dom R )
48	33, 47	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
49	48	adantlr 719	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
50		simpr 462	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) e. RR )
51	18, 25, 49, 50	esumcvgre 28751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
52	51	adantlr 719	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( M ` A ) e. RR )
53	52	adantlr 719	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) e. RR )
54		rpssre 11312	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ RR
55		simplr 760	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
56		2rp 11307	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR+
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. RR+ )
58		df-f1 5606	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
59	58	simplbi 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X -1-1-> NN -> f : X --> NN )
60	59	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> f : X --> NN )
61	60	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. NN )
62	61	nnzd 11039	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
63	57, 62	rpexpcld 12436	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
64	63	adantlr 719	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
65	55, 64	rpdivcld 11358	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR+ )
66	54, 65	sseldi 3468	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
67	66	adantl3r 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
68		rexadd 11525	. . . . . . . . . . . . . . . . 17 |- ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
69	53, 67, 68	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
70	9, 48	sylan 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
71		dfrp2 28188	. . . . . . . . . . . . . . . . . . . 20 |- RR+ = ( 0 (,) +oo )
72		ioossicc 11720	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) +oo ) C_ ( 0 [,] +oo )
73	71, 72	eqsstri 3500	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ ( 0 [,] +oo )
74	73, 65	sseldi 3468	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
75	74	adantl3r 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
76	70, 75	xrge0addcld 28183	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
77	69, 76	eqeltrrd 2518	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
78	54, 55	sseldi 3468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
79	78	adantl3r 754	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
80	54, 63	sseldi 3468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
81	80	adantlr 719	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
82	81	adantl3r 754	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
83		simplr 760	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
84	83	rpgt0d 11344	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
85		2re 10679	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR
86	85	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 2 e. RR )
87	62	adantllr 723	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
88	87	adantlr 719	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( f ` y ) e. ZZ )
89		2pos 10701	. . . . . . . . . . . . . . . . . . . . 21 |- 0 < 2
90	89	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < 2 )
91		expgt0 12302	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
92	86, 88, 90, 91	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < ( 2 ^ ( f ` y ) ) )
93	79, 82, 84, 92	divgt0d 10542	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < ( e / ( 2 ^ ( f ` y ) ) ) )
94	67, 53	ltaddposd 10196	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 0 < ( e / ( 2 ^ ( f ` y ) ) ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
95	93, 94	mpbid 213	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
96		ovex 6333	. . . . . . . . . . . . . . . . . 18 |- ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. _V
97		fvex 5891	. . . . . . . . . . . . . . . . . 18 |- ( M ` A ) e. _V
98	96, 97	brcnv 5037	. . . . . . . . . . . . . . . . 17 |- ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < ( M ` A ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
99	95, 98	sylibr 215	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < ( M ` A ) )
100	29	fveq1i 5882	. . . . . . . . . . . . . . . . . 18 |- ( M ` A ) = ( (toOMeas ` R ) ` A )
101	26	adantr 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. X ) -> Q e. V )
102	27	adantr 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
103		omsfval 28955	. . . . . . . . . . . . . . . . . . 19 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( (toOMeas ` R ) ` A ) = sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
104	101, 102, 34, 103	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. X ) -> ( (toOMeas ` R ) ` A ) = sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
105	100, 104	syl5eq 2482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. X ) -> ( M ` A ) = sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
106	9, 105	sylan 473	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) = sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
107	99, 106	breqtrd 4450	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
108	77, 107	jca 534	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) ) )
109		iccssxr 11717	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
110		xrltso 11440	. . . . . . . . . . . . . . . . . . 19 |- < Or RR*
111		soss 4793	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
112	109, 110, 111	mp2 9	. . . . . . . . . . . . . . . . . 18 |- < Or ( 0 [,] +oo )
113		cnvso 5395	. . . . . . . . . . . . . . . . . 18 |- ( < Or ( 0 [,] +oo ) <-> `' < Or ( 0 [,] +oo ) )
114	112, 113	mpbi 211	. . . . . . . . . . . . . . . . 17 |- `' < Or ( 0 [,] +oo )
115	114	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> `' < Or ( 0 [,] +oo ) )
116		omscl 28956	. . . . . . . . . . . . . . . . . 18 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
117	101, 102, 47, 116	syl3anc 1264	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. X ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
118		xrge0infss 28181	. . . . . . . . . . . . . . . . 17 |- ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. e `' < t /\ A. t e. ( 0 [,] +oo ) ( t `' < e -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) t `' < u ) ) )
119	117, 118	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. e `' < t /\ A. t e. ( 0 [,] +oo ) ( t `' < e -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) t `' < u ) ) )
120	115, 119	suplub 7980	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. X ) -> ( ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
121	120	imp 430	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. X ) /\ ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < sup ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u )
122	23, 24, 108, 121	syl21anc 1263	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u )
123		eqid 2429	. . . . . . . . . . . . . . . . . . 19 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) = ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) )
124		esumex 28689	. . . . . . . . . . . . . . . . . . 19 |- Σ* w e. x ( R ` w ) e. _V
125	123, 124	elrnmpti 5105	. . . . . . . . . . . . . . . . . 18 |- ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } u = Σ* w e. x ( R ` w ) )
126	125	anbi1i 699	. . . . . . . . . . . . . . . . 17 |- ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
127		r19.41v 2987	. . . . . . . . . . . . . . . . 17 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
128	126, 127	bitr4i 255	. . . . . . . . . . . . . . . 16 |- ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
129	128	exbii 1714	. . . . . . . . . . . . . . 15 |- ( E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
130		df-rex 2788	. . . . . . . . . . . . . . 15 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u <-> E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
131		rexcom4 3107	. . . . . . . . . . . . . . 15 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
132	129, 130, 131	3bitr4i 280	. . . . . . . . . . . . . 14 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) )
133		simpr 462	. . . . . . . . . . . . . . . . 17 |- ( ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u )
134		simpl 458	. . . . . . . . . . . . . . . . 17 |- ( ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> u = Σ* w e. x ( R ` w ) )
135	133, 134	breqtrd 4450	. . . . . . . . . . . . . . . 16 |- ( ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) )
136	135	exlimiv 1769	. . . . . . . . . . . . . . 15 |- ( E. u ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) )
137	136	reximi 2900	. . . . . . . . . . . . . 14 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) )
138	132, 137	sylbi 198	. . . . . . . . . . . . 13 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) )
139	122, 138	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) )
140		simpr 462	. . . . . . . . . . . . . . . 16 |- ( ( A C_ U. z /\ z ~<_ om ) -> z ~<_ om )
141	140	a1i 11	. . . . . . . . . . . . . . 15 |- ( z e. ~P dom R -> ( ( A C_ U. z /\ z ~<_ om ) -> z ~<_ om ) )
142	141	ss2rabi 3549	. . . . . . . . . . . . . 14 |- { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } C_ { z e. ~P dom R | z ~<_ om }
143		rexss 3534	. . . . . . . . . . . . . 14 |- ( { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } C_ { z e. ~P dom R | z ~<_ om } -> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) <-> E. x e. { z e. ~P dom R | z ~<_ om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) )
144	142, 143	ax-mp 5	. . . . . . . . . . . . 13 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) <-> E. x e. { z e. ~P dom R | z ~<_ om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) )
145		unieq 4230	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> U. z = U. x )
146	145	sseq2d 3498	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
147		breq1 4429	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( z ~<_ om <-> x ~<_ om ) )
148	146, 147	anbi12d 715	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( A C_ U. z /\ z ~<_ om ) <-> ( A C_ U. x /\ x ~<_ om ) ) )
149	148	elrab 3235	. . . . . . . . . . . . . . . . . 18 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } <-> ( x e. ~P dom R /\ ( A C_ U. x /\ x ~<_ om ) ) )
150	149	simprbi 465	. . . . . . . . . . . . . . . . 17 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> ( A C_ U. x /\ x ~<_ om ) )
151	150	simpld 460	. . . . . . . . . . . . . . . 16 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> A C_ U. x )
152	151	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> A C_ U. x ) )
153	152	anim1d 566	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) -> ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) )
154	153	reximdv 2906	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( E. x e. { z e. ~P dom R | z ~<_ om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) )
155	144, 154	syl5bi 220	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) )
156	139, 155	mpd 15	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) )
157	156	ex 435	. . . . . . . . . 10 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( y e. X -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) )
158	22, 157	ralrimi 2832	. . . . . . . . 9 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. y e. X E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) )
159		unieq 4230	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
160	159	sseq2d 3498	. . . . . . . . . . . 12 |- ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
161		esumeq1 28694	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> Σ* w e. x ( R ` w ) = Σ* w e. ( g ` y ) ( R ` w ) )
162	161	breq2d 4438	. . . . . . . . . . . 12 |- ( x = ( g ` y ) -> ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) <-> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) )
163	160, 162	anbi12d 715	. . . . . . . . . . 11 |- ( x = ( g ` y ) -> ( ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) <-> ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) )
164	163	ac6sg 8916	. . . . . . . . . 10 |- ( X e. _V -> ( A. y e. X E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) ) )
165	164	imp 430	. . . . . . . . 9 |- ( ( X e. _V /\ A. y e. X E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. x ( R ` w ) ) ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) )
166	12, 158, 165	syl2anc 665	. . . . . . . 8 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) )
167	9	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ph )
168	39	ralrimiva 2846	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. y e. X A C_ U. dom R )
169		iunss 4343	. . . . . . . . . . . . . . . . . 18 |- ( U_ y e. X A C_ U. dom R <-> A. y e. X A C_ U. dom R )
170	168, 169	sylibr 215	. . . . . . . . . . . . . . . . 17 |- ( ph -> U_ y e. X A C_ U. dom R )
171	44	ralrimiva 2846	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. y e. X A e. _V )
172		iunexg 6783	. . . . . . . . . . . . . . . . . . 19 |- ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
173	11, 171, 172	syl2anc 665	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U_ y e. X A e. _V )
174		elpwg 3993	. . . . . . . . . . . . . . . . . 18 |- ( U_ y e. X A e. _V -> ( U_ y e. X A e. ~P U. dom R <-> U_ y e. X A C_ U. dom R ) )
175	173, 174	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( U_ y e. X A e. ~P U. dom R <-> U_ y e. X A C_ U. dom R ) )
176	170, 175	mpbird 235	. . . . . . . . . . . . . . . 16 |- ( ph -> U_ y e. X A e. ~P U. dom R )
177	32, 176	ffvelrnd 6038	. . . . . . . . . . . . . . 15 |- ( ph -> ( M ` U_ y e. X A ) e. ( 0 [,] +oo ) )
178	109, 177	sseldi 3468	. . . . . . . . . . . . . 14 |- ( ph -> ( M ` U_ y e. X A ) e. RR* )
179	167, 178	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ( M ` U_ y e. X A ) e. RR* )
180		simplr 760	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
181	25	ad4antr 736	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> X e. _V )
182		fex 6153	. . . . . . . . . . . . . . . . 17 |- ( ( g : X --> { z e. ~P dom R | z ~<_ om } /\ X e. _V ) -> g e. _V )
183	180, 181, 182	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> g e. _V )
184		rnexg 6739	. . . . . . . . . . . . . . . 16 |- ( g e. _V -> ran g e. _V )
185		uniexg 6602	. . . . . . . . . . . . . . . 16 |- ( ran g e. _V -> U. ran g e. _V )
186	183, 184, 185	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U. ran g e. _V )
187		simp-5l 776	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ph )
188	27	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
189		frn 5752	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ { z e. ~P dom R | z ~<_ om } )
190		ssrab2 3552	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { z e. ~P dom R | z ~<_ om } C_ ~P dom R
191	189, 190	syl6ss 3482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
192	191	unissd 4246	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ U. ~P dom R )
193		unipw 4672	. . . . . . . . . . . . . . . . . . . . . 22 |- U. ~P dom R = dom R
194	192, 193	syl6sseq 3516	. . . . . . . . . . . . . . . . . . . . 21 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
195	194	adantl 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ dom R )
196	36	adantr 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> dom R = Q )
197	195, 196	sseqtrd 3506	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ Q )
198	197	sselda 3470	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> c e. Q )
199	188, 198	ffvelrnd 6038	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> ( R ` c ) e. ( 0 [,] +oo ) )
200	199	ralrimiva 2846	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
201	187, 180, 200	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
202		nfcv 2591	. . . . . . . . . . . . . . . 16 |- F/_ c U. ran g
203	202	esumcl 28690	. . . . . . . . . . . . . . 15 |- ( ( U. ran g e. _V /\ A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) ) -> Σ* c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
204	186, 201, 203	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> Σ* c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
205	109, 204	sseldi 3468	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> Σ* c e. U. ran g ( R ` c ) e. RR* )
206		simp-5r 777	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> Σ* y e. X ( M ` A ) e. RR )
207	206	rexrd 9689	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> Σ* y e. X ( M ` A ) e. RR* )
208		simpllr 767	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> e e. RR+ )
209	208	rpxrd 11342	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> e e. RR* )
210	207, 209	xaddcld 11587	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> (Σ* y e. X ( M ` A ) +e e ) e. RR* )
211	189	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ran g C_ { z e. ~P dom R | z ~<_ om } )
212		sstr 3478	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran g C_ { z e. ~P dom R | z ~<_ om } /\ { z e. ~P dom R | z ~<_ om } C_ ~P dom R ) -> ran g C_ ~P dom R )
213	190, 212	mpan2 675	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
214		sspwuni 4391	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
215	213, 214	sylib 199	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
216	211, 215	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U. ran g C_ dom R )
217		ffn 5746	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> g Fn X )
218	217	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> g Fn X )
219	167, 1	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> X ~<_ om )
220		fnct 28140	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g Fn X /\ X ~<_ om ) -> g ~<_ om )
221		rnct 28143	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( g ~<_ om -> ran g ~<_ om )
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g Fn X /\ X ~<_ om ) -> ran g ~<_ om )
223		dfss3 3460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } <-> A. w e. ran g w e. { z e. ~P dom R | z ~<_ om } )
224	223	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> A. w e. ran g w e. { z e. ~P dom R | z ~<_ om } )
225		breq1 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = w -> ( z ~<_ om <-> w ~<_ om ) )
226	225	elrab 3235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. { z e. ~P dom R | z ~<_ om } <-> ( w e. ~P dom R /\ w ~<_ om ) )
227	226	simprbi 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( w e. { z e. ~P dom R | z ~<_ om } -> w ~<_ om )
228	227	ralimi 2825	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. w e. ran g w e. { z e. ~P dom R | z ~<_ om } -> A. w e. ran g w ~<_ om )
229	224, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> A. w e. ran g w ~<_ om )
230		unictb 8998	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran g ~<_ om /\ A. w e. ran g w ~<_ om ) -> U. ran g ~<_ om )
231	222, 229, 230	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( g Fn X /\ X ~<_ om ) /\ ran g C_ { z e. ~P dom R | z ~<_ om } ) -> U. ran g ~<_ om )
232	218, 219, 211, 231	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U. ran g ~<_ om )
233		ctex 28135	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g ~<_ om -> U. ran g e. _V )
234		elpwg 3993	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g e. _V -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
235	232, 233, 234	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
236	216, 235	mpbird 235	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U. ran g e. ~P dom R )
237		simpl 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) -> A C_ U. ( g ` y ) )
238	237	ralimi 2825	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) -> A. y e. X A C_ U. ( g ` y ) )
239		fvssunirn 5904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g ` y ) C_ U. ran g
240	239	unissi 4245	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U. ( g ` y ) C_ U. U. ran g
241		sstr 3478	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
242	240, 241	mpan2 675	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
243	242	ralimi 2825	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
244		iunss 4343	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( U_ y e. X A C_ U. U. ran g <-> A. y e. X A C_ U. U. ran g )
245	243, 244	sylibr 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. X A C_ U. ( g ` y ) -> U_ y e. X A C_ U. U. ran g )
246	238, 245	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) -> U_ y e. X A C_ U. U. ran g )
247	246	adantl 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U_ y e. X A C_ U. U. ran g )
248	236, 247, 232	jca32 537	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ( U. ran g e. ~P dom R /\ ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ om ) ) )
249		unieq 4230	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = U. ran g -> U. z = U. U. ran g )
250	249	sseq2d 3498	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( U_ y e. X A C_ U. z <-> U_ y e. X A C_ U. U. ran g ) )
251		breq1 4429	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( z ~<_ om <-> U. ran g ~<_ om ) )
252	250, 251	anbi12d 715	. . . . . . . . . . . . . . . . . . . 20 |- ( z = U. ran g -> ( ( U_ y e. X A C_ U. z /\ z ~<_ om ) <-> ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ om ) ) )
253	252	elrab 3235	. . . . . . . . . . . . . . . . . . 19 |- ( U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } <-> ( U. ran g e. ~P dom R /\ ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ om ) ) )
254	248, 253	sylibr 215	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } )
255		fveq2 5881	. . . . . . . . . . . . . . . . . . 19 |- ( c = w -> ( R ` c ) = ( R ` w ) )
256	255	cbvesumv 28703	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w )
257		esumeq1 28694	. . . . . . . . . . . . . . . . . . . 20 |- ( x = U. ran g -> Σ* w e. x ( R ` w ) = Σ* w e. U. ran g ( R ` w ) )
258	257	eqeq2d 2443	. . . . . . . . . . . . . . . . . . 19 |- ( x = U. ran g -> (Σ* c e. U. ran g ( R ` c ) = Σ* w e. x ( R ` w ) <-> Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w ) ) )
259	258	rspcev 3188	. . . . . . . . . . . . . . . . . 18 |- ( ( U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } /\ Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w ) ) -> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) }Σ* c e. U. ran g ( R ` c ) = Σ* w e. x ( R ` w ) )
260	254, 256, 259	sylancl 666	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) }Σ* c e. U. ran g ( R ` c ) = Σ* w e. x ( R ` w ) )
261		esumex 28689	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) e. _V
262		eqid 2429	. . . . . . . . . . . . . . . . . . 19 |- ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) = ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) )
263	262	elrnmpt 5101	. . . . . . . . . . . . . . . . . 18 |- (Σ* c e. U. ran g ( R ` c ) e. _V -> (Σ* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) }Σ* c e. U. ran g ( R ` c ) = Σ* w e. x ( R ` w ) ) )
264	261, 263	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- (Σ* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) <-> E. x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) }Σ* c e. U. ran g ( R ` c ) = Σ* w e. x ( R ` w ) )
265	260, 264	sylibr 215	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> Σ* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) )
266	114	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> `' < Or ( 0 [,] +oo ) )
267		omscl 28956	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ U_ y e. X A e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
268	26, 27, 176, 267	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) )
269		xrge0infss 28181	. . . . . . . . . . . . . . . . . . 19 |- ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. e `' < t /\ A. t e. ( 0 [,] +oo ) ( t `' < e -> E. u e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) t `' < u ) ) )
270	268, 269	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> E. e e. ( 0 [,] +oo ) ( A. t e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. e `' < t /\ A. t e. ( 0 [,] +oo ) ( t `' < e -> E. u e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) t `' < u ) ) )
271	266, 270	supub 7979	. . . . . . . . . . . . . . . . 17 |- ( ph -> (Σ* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -> -. sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) `' < Σ* c e. U. ran g ( R ` c ) ) )
272	29	fveq1i 5882	. . . . . . . . . . . . . . . . . . . 20 |- ( M ` U_ y e. X A ) = ( (toOMeas ` R ) ` U_ y e. X A )
273	170, 37	sseqtrd 3506	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U_ y e. X A C_ U. Q )
274		omsfval 28955	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ U_ y e. X A C_ U. Q ) -> ( (toOMeas ` R ) ` U_ y e. X A ) = sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
275	26, 27, 273, 274	syl3anc 1264	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( (toOMeas ` R ) ` U_ y e. X A ) = sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
276	272, 275	syl5eq 2482	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M ` U_ y e. X A ) = sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) )
277	276	breq1d 4436	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) <-> sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) `' < Σ* c e. U. ran g ( R ` c ) ) )
278	277	notbid 295	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) <-> -. sup ( ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , `' < ) `' < Σ* c e. U. ran g ( R ` c ) ) )
279	271, 278	sylibrd 237	. . . . . . . . . . . . . . . 16 |- ( ph -> (Σ* c e. U. ran g ( R ` c ) e. ran ( x e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -> -. ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) ) )
280	167, 265, 279	sylc 62	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> -. ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) )
281		fvex 5891	. . . . . . . . . . . . . . . . 17 |- ( M ` U_ y e. X A ) e. _V
282	281, 261	brcnv 5037	. . . . . . . . . . . . . . . 16 |- ( ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) <-> Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
283	282	notbii 297	. . . . . . . . . . . . . . 15 |- ( -. ( M ` U_ y e. X A ) `' < Σ* c e. U. ran g ( R ` c ) <-> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
284	280, 283	sylib 199	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
285		xrlenlt 9698	. . . . . . . . . . . . . . 15 |- ( ( ( M ` U_ y e. X A ) e. RR* /\ Σ* c e. U. ran g ( R ` c ) e. RR* ) -> ( ( M ` U_ y e. X A ) <_ Σ* c e. U. ran g ( R ` c ) <-> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
286	179, 205, 285	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ( ( M ` U_ y e. X A ) <_ Σ* c e. U. ran g ( R ` c ) <-> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
287	284, 286	mpbird 235	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) -> ( M ` U_ y e. X A ) <_ Σ* c e. U. ran g ( R ` c ) )
288		nfv 1754	. . . . . . . . . . . . . . . . . . 19 |- F/ y g : X --> { z e. ~P dom R | z ~<_ om }
289	22, 288	nfan 1986	. . . . . . . . . . . . . . . . . 18 |- F/ y ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } )
290		nfra1 2813	. . . . . . . . . . . . . . . . . 18 |- F/ y A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) )
291	289, 290	nfan 1986	. . . . . . . . . . . . . . . . 17 |- F/ y ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) )
292		simp-6l 778	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) /\ y e. X ) -> ph )
293		simpllr 767	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) /\ y e. X ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
294		simpr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ A. y e. X ( A C_ U. ( g ` y ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < Σ* w e. ( g ` y ) ( R ` w ) ) ) /\ y e. X ) -> y e. X )
295	27	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
296		simpllr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
297		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> y e. X )
298	296, 297	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. { z e. ~P dom R | z ~<_ om } )
299	190, 298	sseldi 3468	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. ~P dom R )
300	299	elpwid 3995	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ dom R )
301	295, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> dom R = Q )
302	300, 301	sseqtrd 3506	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
303		simpr 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. ( g ` y ) )
304	302, 303	sseldd 3471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. Q )
305	295, 304	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( R ` w ) e. ( 0 [,] +oo ) )
306	305	ralrimiva 2846	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) -> A. w e. ( g ` y )