Theorem omssubaddOLD 29205

Description: A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) Obsolete version of omssubadd 29201 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
omssubaddOLD	|- ( 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 omssubaddOLD

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		omssubaddOLD.b	. . . . . 6 |- ( ph -> X ~<_ om )
2		nnenom 12231	. . . . . . 7 |- NN ~~ om
3	2	ensymi 7637	. . . . . 6 |- om ~~ NN
4		domentr 7646	. . . . . 6 |- ( ( X ~<_ om /\ om ~~ NN ) -> X ~<_ NN )
5	1, 3, 4	sylancl 675	. . . . 5 |- ( ph -> X ~<_ NN )
6		brdomi 7598	. . . . 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 472	. . 3 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> E. f f : X -1-1-> NN )
9		simplll 776	. . . . . . . . . 10 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ph )
10		ctex 7602	. . . . . . . . . . 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 1769	. . . . . . . . . . . . 13 |- F/ y ph
14		nfcv 2612	. . . . . . . . . . . . . . 15 |- F/_ y X
15	14	nfesum1 28935	. . . . . . . . . . . . . 14 |- F/_ yΣ* y e. X ( M ` A )
16		nfcv 2612	. . . . . . . . . . . . . 14 |- F/_ y RR
17	15, 16	nfel 2624	. . . . . . . . . . . . 13 |- F/ yΣ* y e. X ( M ` A ) e. RR
18	13, 17	nfan 2031	. . . . . . . . . . . 12 |- F/ y ( ph /\ Σ* y e. X ( M ` A ) e. RR )
19		nfv 1769	. . . . . . . . . . . 12 |- F/ y f : X -1-1-> NN
20	18, 19	nfan 2031	. . . . . . . . . . 11 |- F/ y ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
21		nfv 1769	. . . . . . . . . . 11 |- F/ y e e. RR+
22	20, 21	nfan 2031	. . . . . . . . . 10 |- F/ y ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
23	9	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
24		simpr 468	. . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> X e. _V )
26		omsOLD.o	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> Q e. V )
27		omsOLD.r	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> R : Q --> ( 0 [,] +oo ) )
28		omsfOLD 29197	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
29		omsOLD.m	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- M = (toOMeas ` R )
30	29	feq1i 5730	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
31	28, 30	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
32	26, 27, 31	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
33	32	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. X ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
34		omssubaddOLD.a	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A C_ U. Q )
35		fdm 5745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
36	27, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> dom R = Q )
37	36	unieqd 4200	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> U. dom R = U. Q )
38	37	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> U. dom R = U. Q )
39	34, 38	sseqtr4d 3455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. X ) -> A C_ U. dom R )
40		uniexg 6607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( Q e. V -> U. Q e. _V )
41	26, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> U. Q e. _V )
42	41	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. X ) -> U. Q e. _V )
43		ssexg 4542	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
44	34, 42, 43	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A e. _V )
45		elpwg 3950	. . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
50		simpr 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) e. RR )
51	18, 25, 49, 50	esumcvgre 28986	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
52	51	adantlr 729	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( M ` A ) e. RR )
53	52	adantlr 729	. . . . . . . . . . . . . . . . 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 11335	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ RR
55		simplr 770	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
56		2rp 11330	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR+
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. RR+ )
58		df-f1 5594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
59	58	simplbi 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X -1-1-> NN -> f : X --> NN )
60	59	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 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 11062	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
63	57, 62	rpexpcld 12477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
64	63	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
65	55, 64	rpdivcld 11381	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR+ )
66	54, 65	sseldi 3416	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
67	66	adantl3r 764	. . . . . . . . . . . . . . . . 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 11548	. . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . 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 28427	. . . . . . . . . . . . . . . . . . . 20 |- RR+ = ( 0 (,) +oo )
72		ioossicc 11745	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) +oo ) C_ ( 0 [,] +oo )
73	71, 72	eqsstri 3448	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ ( 0 [,] +oo )
74	73, 65	sseldi 3416	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
75	74	adantl3r 764	. . . . . . . . . . . . . . . . 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 28419	. . . . . . . . . . . . . . . 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 2550	. . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
79	78	adantl3r 764	. . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
81	80	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
82	81	adantl3r 764	. . . . . . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . . 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 11367	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
85		2re 10701	. . . . . . . . . . . . . . . . . . . . 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 733	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
88	87	adantlr 729	. . . . . . . . . . . . . . . . . . . 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 10723	. . . . . . . . . . . . . . . . . . . . 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 12343	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
92	86, 88, 90, 91	syl3anc 1292	. . . . . . . . . . . . . . . . . . 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 10564	. . . . . . . . . . . . . . . . . 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 10218	. . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . 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 6336	. . . . . . . . . . . . . . . . . 18 |- ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. _V
97		fvex 5889	. . . . . . . . . . . . . . . . . 18 |- ( M ` A ) e. _V
98	96, 97	brcnv 5022	. . . . . . . . . . . . . . . . 17 |- ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < ( M ` A ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
99	95, 98	sylibr 217	. . . . . . . . . . . . . . . 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 5880	. . . . . . . . . . . . . . . . . 18 |- ( M ` A ) = ( (toOMeas ` R ) ` A )
101	26	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. X ) -> Q e. V )
102	27	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
103		omsfvalOLD 29195	. . . . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . . . 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 2517	. . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . 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 4420	. . . . . . . . . . . . . . 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 541	. . . . . . . . . . . . . 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 11742	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
110		xrltso 11463	. . . . . . . . . . . . . . . . . . 19 |- < Or RR*
111		soss 4778	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
112	109, 110, 111	mp2 9	. . . . . . . . . . . . . . . . . 18 |- < Or ( 0 [,] +oo )
113		cnvso 5382	. . . . . . . . . . . . . . . . . 18 |- ( < Or ( 0 [,] +oo ) <-> `' < Or ( 0 [,] +oo ) )
114	112, 113	mpbi 213	. . . . . . . . . . . . . . . . 17 |- `' < Or ( 0 [,] +oo )
115	114	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> `' < Or ( 0 [,] +oo ) )
116		omsclOLD 29196	. . . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . . 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		xrge0infssOLD 28416	. . . . . . . . . . . . . . . . 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 7992	. . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . 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 1291	. . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . . . . . 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 28924	. . . . . . . . . . . . . . . . . . 19 |- Σ* w e. x ( R ` w ) e. _V
125	123, 124	elrnmpti 5091	. . . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . . 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 2928	. . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . 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 1726	. . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . 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 3053	. . . . . . . . . . . . . . 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 285	. . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . 17 |- ( ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u )
134		simpl 464	. . . . . . . . . . . . . . . . 17 |- ( ( u = Σ* w e. x ( R ` w ) /\ ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) `' < u ) -> u = Σ* w e. x ( R ` w ) )
135	133, 134	breqtrd 4420	. . . . . . . . . . . . . . . 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 1784	. . . . . . . . . . . . . . 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 2852	. . . . . . . . . . . . . 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 200	. . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . 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 3497	. . . . . . . . . . . . . 14 |- { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } C_ { z e. ~P dom R | z ~<_ om }
143		rexss 3482	. . . . . . . . . . . . . 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 4198	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> U. z = U. x )
146	145	sseq2d 3446	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
147		breq1 4398	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( z ~<_ om <-> x ~<_ om ) )
148	146, 147	anbi12d 725	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( A C_ U. z /\ z ~<_ om ) <-> ( A C_ U. x /\ x ~<_ om ) ) )
149	148	elrab 3184	. . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . 17 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> ( A C_ U. x /\ x ~<_ om ) )
151	150	simpld 466	. . . . . . . . . . . . . . . 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 574	. . . . . . . . . . . . . 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 2857	. . . . . . . . . . . . 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 225	. . . . . . . . . . . 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 441	. . . . . . . . . 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 2800	. . . . . . . . 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 4198	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
160	159	sseq2d 3446	. . . . . . . . . . . 12 |- ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
161		esumeq1 28929	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> Σ* w e. x ( R ` w ) = Σ* w e. ( g ` y ) ( R ` w ) )
162	161	breq2d 4407	. . . . . . . . . . . 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 725	. . . . . . . . . . 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 8936	. . . . . . . . . 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 436	. . . . . . . . 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 673	. . . . . . . 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 740	. . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. y e. X A C_ U. dom R )
169		iunss 4310	. . . . . . . . . . . . . . . . . 18 |- ( U_ y e. X A C_ U. dom R <-> A. y e. X A C_ U. dom R )
170	168, 169	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ( ph -> U_ y e. X A C_ U. dom R )
171	44	ralrimiva 2809	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. y e. X A e. _V )
172		iunexg 6788	. . . . . . . . . . . . . . . . . . 19 |- ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
173	11, 171, 172	syl2anc 673	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U_ y e. X A e. _V )
174		elpwg 3950	. . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . 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 746	. . . . . . . . . . . . . . . . 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 6155	. . . . . . . . . . . . . . . . 17 |- ( ( g : X --> { z e. ~P dom R | z ~<_ om } /\ X e. _V ) -> g e. _V )
183	180, 181, 182	syl2anc 673	. . . . . . . . . . . . . . . 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 6744	. . . . . . . . . . . . . . . 16 |- ( g e. _V -> ran g e. _V )
185		uniexg 6607	. . . . . . . . . . . . . . . 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 786	. . . . . . . . . . . . . . . 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 740	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
189		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ { z e. ~P dom R | z ~<_ om } )
190		ssrab2 3500	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { z e. ~P dom R | z ~<_ om } C_ ~P dom R
191	189, 190	syl6ss 3430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
192	191	unissd 4214	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ U. ~P dom R )
193		unipw 4650	. . . . . . . . . . . . . . . . . . . . . 22 |- U. ~P dom R = dom R
194	192, 193	syl6sseq 3464	. . . . . . . . . . . . . . . . . . . . 21 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
195	194	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ dom R )
196	36	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> dom R = Q )
197	195, 196	sseqtrd 3454	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ Q )
198	197	sselda 3418	. . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . 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 2612	. . . . . . . . . . . . . . . 16 |- F/_ c U. ran g
203	202	esumcl 28925	. . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . 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 787	. . . . . . . . . . . . . . 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 9708	. . . . . . . . . . . . . 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 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 ) ) ) -> e e. RR+ )
209	208	rpxrd 11365	. . . . . . . . . . . . . 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 11612	. . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . . . . . . 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 3426	. . . . . . . . . . . . . . . . . . . . . . . 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 685	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
214		sspwuni 4360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
215	213, 214	sylib 201	. . . . . . . . . . . . . . . . . . . . . 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 5739	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> g Fn X )
218	217	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . 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 28372	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g Fn X /\ X ~<_ om ) -> g ~<_ om )
221		rnct 28375	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( g ~<_ om -> ran g ~<_ om )
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g Fn X /\ X ~<_ om ) -> ran g ~<_ om )
223		dfss3 3408	. . . . . . . . . . . . . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = w -> ( z ~<_ om <-> w ~<_ om ) )
226	225	elrab 3184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. { z e. ~P dom R | z ~<_ om } <-> ( w e. ~P dom R /\ w ~<_ om ) )
227	226	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( w e. { z e. ~P dom R | z ~<_ om } -> w ~<_ om )
228	227	ralimi 2796	. . . . . . . . . . . . . . . . . . . . . . . . 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 9018	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran g ~<_ om /\ A. w e. ran g w ~<_ om ) -> U. ran g ~<_ om )
231	222, 229, 230	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . 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 1291	. . . . . . . . . . . . . . . . . . . . . 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 7602	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g ~<_ om -> U. ran g e. _V )
234		elpwg 3950	. . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . . . . . . . . . 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 5902	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g ` y ) C_ U. ran g
240	239	unissi 4213	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U. ( g ` y ) C_ U. U. ran g
241		sstr 3426	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
242	240, 241	mpan2 685	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
243	242	ralimi 2796	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
244		iunss 4310	. . . . . . . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . . . . . . 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 544	. . . . . . . . . . . . . . . . . . 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 4198	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = U. ran g -> U. z = U. U. ran g )
250	249	sseq2d 3446	. . . . . . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( z ~<_ om <-> U. ran g ~<_ om ) )
252	250, 251	anbi12d 725	. . . . . . . . . . . . . . . . . . . 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 3184	. . . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . 19 |- ( c = w -> ( R ` c ) = ( R ` w ) )
256	255	cbvesumv 28938	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w )
257		esumeq1 28929	. . . . . . . . . . . . . . . . . . . 20 |- ( x = U. ran g -> Σ* w e. x ( R ` w ) = Σ* w e. U. ran g ( R ` w ) )
258	257	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 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 3136	. . . . . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . . . . 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 28924	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) e. _V
262		eqid 2471	. . . . . . . . . . . . . . . . . . 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 5087	. . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . 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		omsclOLD 29196	. . . . . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . . . . 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		xrge0infssOLD 28416	. . . . . . . . . . . . . . . . . . 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 7991	. . . . . . . . . . . . . . . . 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 5880	. . . . . . . . . . . . . . . . . . . 20 |- ( M ` U_ y e. X A ) = ( (toOMeas ` R ) ` U_ y e. X A )
273	170, 37	sseqtrd 3454	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U_ y e. X A C_ U. Q )
274		omsfvalOLD 29195	. . . . . . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . . . . . 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 2517	. . . . . . . . . . . . . . . . . . 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 4405	. . . . . . . . . . . . . . . . . 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 301	. . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . 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 61	. . . . . . . . . . . . . . 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 5889	. . . . . . . . . . . . . . . . 17 |- ( M ` U_ y e. X A ) e. _V
282	281, 261	brcnv 5022	. . . . . . . . . . . . . . . 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 303	. . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . 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 9717	. . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . 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 240	. . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . . . . 19 |- F/ y g : X --> { z e. ~P dom R | z ~<_ om }
289	22, 288	nfan 2031	. . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . . . . 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 2031	. . . . . . . . . . . . . . . . 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 788	. . . . . . . . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . 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 744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
296		simpllr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . . . . . . 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 3952	. . . . . . . . . . . . . . . . . . . . . . . 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 3454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
303		simpr 468	. . . . . . . . . . . . . . . . . . . . . . 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 3419	. . . . . . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) -> A.