Theorem omssubadd 30362

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

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 h v c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		omssubadd.b	. . . . . 6 |- ( ph -> X ~<_ om )
2		nnenom 12779	. . . . . . 7 |- NN ~~ om
3	2	ensymi 8006	. . . . . 6 |- om ~~ NN
4		domentr 8015	. . . . . 6 |- ( ( X ~<_ om /\ om ~~ NN ) -> X ~<_ NN )
5	1, 3, 4	sylancl 694	. . . . 5 |- ( ph -> X ~<_ NN )
6		brdomi 7966	. . . . 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 481	. . 3 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> E. f f : X -1-1-> NN )
9		simplll 798	. . . . . . . . . 10 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ph )
10		ctex 7970	. . . . . . . . . . 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 1843	. . . . . . . . . . . . 13 |- F/ y ph
14		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ y X
15	14	nfesum1 30102	. . . . . . . . . . . . . 14 |- F/_ yΣ* y e. X ( M ` A )
16		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ y RR
17	15, 16	nfel 2777	. . . . . . . . . . . . 13 |- F/ yΣ* y e. X ( M ` A ) e. RR
18	13, 17	nfan 1828	. . . . . . . . . . . 12 |- F/ y ( ph /\ Σ* y e. X ( M ` A ) e. RR )
19		nfv 1843	. . . . . . . . . . . 12 |- F/ y f : X -1-1-> NN
20	18, 19	nfan 1828	. . . . . . . . . . 11 |- F/ y ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN )
21		nfv 1843	. . . . . . . . . . 11 |- F/ y e e. RR+
22	20, 21	nfan 1828	. . . . . . . . . 10 |- F/ y ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ )
23	9	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ph )
24		simpr 477	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . 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 30358	. . . . . . . . . . . . . . . . . . . . . . . . 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 6036	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( M : ~P U. dom R --> ( 0 [,] +oo ) <-> (toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
31	28, 30	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> M : ~P U. dom R --> ( 0 [,] +oo ) )
32	26, 27, 31	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M : ~P U. dom R --> ( 0 [,] +oo ) )
33	32	adantr 481	. . . . . . . . . . . . . . . . . . . . . 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 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
36	27, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> dom R = Q )
37	36	unieqd 4446	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> U. dom R = U. Q )
38	37	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> U. dom R = U. Q )
39	34, 38	sseqtr4d 3642	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. X ) -> A C_ U. dom R )
40		uniexg 6955	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( Q e. V -> U. Q e. _V )
41	26, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> U. Q e. _V )
42	41	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. X ) -> U. Q e. _V )
43		ssexg 4804	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
44	34, 42, 43	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. X ) -> A e. _V )
45		elpwg 4166	. . . . . . . . . . . . . . . . . . . . . . . 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 247	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. X ) -> A e. ~P U. dom R )
48	33, 47	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
49	48	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
50		simpr 477	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) e. RR )
51	18, 25, 49, 50	esumcvgre 30153	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ y e. X ) -> ( M ` A ) e. RR )
52	51	adantlr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( M ` A ) e. RR )
53	52	adantlr 751	. . . . . . . . . . . . . . . . 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 11843	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ RR
55		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR+ )
56		2rp 11837	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR+
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. RR+ )
58		df-f1 5893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN <-> ( f : X --> NN /\ Fun `' f ) )
59	58	simplbi 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X -1-1-> NN -> f : X --> NN )
60	59	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> f : X --> NN )
61	60	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. NN )
62	61	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
63	57, 62	rpexpcld 13032	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
64	63	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR+ )
65	55, 64	rpdivcld 11889	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR+ )
66	54, 65	sseldi 3601	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
67	66	adantl3r 786	. . . . . . . . . . . . . . . . 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 12063	. . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . . . 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 29532	. . . . . . . . . . . . . . . . . . . 20 |- RR+ = ( 0 (,) +oo )
72		ioossicc 12259	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) +oo ) C_ ( 0 [,] +oo )
73	71, 72	eqsstri 3635	. . . . . . . . . . . . . . . . . . 19 |- RR+ C_ ( 0 [,] +oo )
74	73, 65	sseldi 3601	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
75	74	adantl3r 786	. . . . . . . . . . . . . . . . 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 29527	. . . . . . . . . . . . . . . 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 2702	. . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. RR )
79	78	adantl3r 786	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 3601	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
81	80	adantlr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. RR )
82	81	adantl3r 786	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 792	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 11875	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < e )
85		2re 11090	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
86	85	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ y e. X ) -> ( f ` y ) e. ZZ )
88	87	adantlr 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 11112	. . . . . . . . . . . . . . . . . . . 20 |- 0 < 2
90	89	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> 0 < 2 )
91		expgt0 12893	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. RR /\ ( f ` y ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( f ` y ) ) )
92	86, 88, 90, 91	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 10959	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 10611	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 222	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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	29	fveq1i 6192	. . . . . . . . . . . . . . . . . . . 20 |- ( M ` A ) = ( (toOMeas ` R ) ` A )
97	26	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> Q e. V )
98	27	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. X ) -> R : Q --> ( 0 [,] +oo ) )
99		omsfval 30356	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( (toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
100	97, 98, 34, 99	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. X ) -> ( (toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
101	96, 100	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. X ) -> ( M ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
102	9, 101	sylan 488	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( M ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) )
103	102	eqcomd 2628	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) = ( M ` A ) )
104	103	breq1d 4663	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> (inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> ( M ` A ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
105	95, 104	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
106	77, 105	jca 554	. . . . . . . . . . . . . 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 ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
107		iccssxr 12256	. . . . . . . . . . . . . . . . . . 19 |- ( 0 [,] +oo ) C_ RR*
108		xrltso 11974	. . . . . . . . . . . . . . . . . . 19 |- < Or RR*
109		soss 5053	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
110	107, 108, 109	mp2 9	. . . . . . . . . . . . . . . . . 18 |- < Or ( 0 [,] +oo )
111		biid 251	. . . . . . . . . . . . . . . . . 18 |- ( < Or ( 0 [,] +oo ) <-> < Or ( 0 [,] +oo ) )
112	110, 111	mpbi 220	. . . . . . . . . . . . . . . . 17 |- < Or ( 0 [,] +oo )
113	112	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> < Or ( 0 [,] +oo ) )
114		omscl 30357	. . . . . . . . . . . . . . . . . 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 ) )
115	97, 98, 47, 114	syl3anc 1326	. . . . . . . . . . . . . . . . 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 ) )
116		xrge0infss 29525	. . . . . . . . . . . . . . . . 17 |- ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) C_ ( 0 [,] +oo ) -> E. v e. ( 0 [,] +oo ) ( A. h e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. h < v /\ A. h e. ( 0 [,] +oo ) ( v < h -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < h ) ) )
117	115, 116	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. X ) -> E. v e. ( 0 [,] +oo ) ( A. h e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) -. h < v /\ A. h e. ( 0 [,] +oo ) ( v < h -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < h ) ) )
118	113, 117	infglb 8396	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. X ) -> ( ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
119	118	imp 445	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ y e. X ) /\ ( ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) /\ inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) , ( 0 [,] +oo ) , < ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
120	23, 24, 106, 119	syl21anc 1325	. . . . . . . . . . . . 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 ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
121		eqid 2622	. . . . . . . . . . . . . . . . . . 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 ) )
122		esumex 30091	. . . . . . . . . . . . . . . . . . 19 |- Σ* w e. x ( R ` w ) e. _V
123	121, 122	elrnmpti 5376	. . . . . . . . . . . . . . . . . 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 ) )
124	123	anbi1i 731	. . . . . . . . . . . . . . . . 17 |- ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
125		r19.41v 3089	. . . . . . . . . . . . . . . . 17 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
126	124, 125	bitr4i 267	. . . . . . . . . . . . . . . 16 |- ( ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
127	126	exbii 1774	. . . . . . . . . . . . . . 15 |- ( E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
128		df-rex 2918	. . . . . . . . . . . . . . 15 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. u ( u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
129		rexcom4 3225	. . . . . . . . . . . . . . 15 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> E. u E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
130	127, 128, 129	3bitr4i 292	. . . . . . . . . . . . . 14 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
131		breq1 4656	. . . . . . . . . . . . . . . . . 18 |- ( u = Σ* w e. x ( R ` w ) -> ( u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
132		idd 24	. . . . . . . . . . . . . . . . . 18 |- ( u = Σ* w e. x ( R ` w ) -> (Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
133	131, 132	sylbid 230	. . . . . . . . . . . . . . . . 17 |- ( u = Σ* w e. x ( R ` w ) -> ( u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
134	133	imp 445	. . . . . . . . . . . . . . . 16 |- ( ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
135	134	exlimiv 1858	. . . . . . . . . . . . . . 15 |- ( E. u ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
136	135	reximi 3011	. . . . . . . . . . . . . 14 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } E. u ( u = Σ* w e. x ( R ` w ) /\ u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
137	130, 136	sylbi 207	. . . . . . . . . . . . 13 |- ( E. u e. ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } |-> Σ* w e. x ( R ` w ) ) u < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
138	120, 137	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 ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
139		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( A C_ U. z /\ z ~<_ om ) -> z ~<_ om )
140	139	a1i 11	. . . . . . . . . . . . . . 15 |- ( z e. ~P dom R -> ( ( A C_ U. z /\ z ~<_ om ) -> z ~<_ om ) )
141	140	ss2rabi 3684	. . . . . . . . . . . . . 14 |- { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } C_ { z e. ~P dom R | z ~<_ om }
142		rexss 3669	. . . . . . . . . . . . . 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 ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | z ~<_ om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
143	141, 142	ax-mp 5	. . . . . . . . . . . . 13 |- ( E. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> E. x e. { z e. ~P dom R | z ~<_ om } ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
144		unieq 4444	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> U. z = U. x )
145	144	sseq2d 3633	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( A C_ U. z <-> A C_ U. x ) )
146		breq1 4656	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( z ~<_ om <-> x ~<_ om ) )
147	145, 146	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( A C_ U. z /\ z ~<_ om ) <-> ( A C_ U. x /\ x ~<_ om ) ) )
148	147	elrab 3363	. . . . . . . . . . . . . . . . . 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 ) ) )
149	148	simprbi 480	. . . . . . . . . . . . . . . . 17 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> ( A C_ U. x /\ x ~<_ om ) )
150	149	simpld 475	. . . . . . . . . . . . . . . 16 |- ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ om ) } -> A C_ U. x )
151	150	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 ) )
152	151	anim1d 588	. . . . . . . . . . . . . 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 ) } /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
153	152	reximdv 3016	. . . . . . . . . . . . 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 ) } /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
154	143, 153	syl5bi 232	. . . . . . . . . . . 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 ) }Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
155	138, 154	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 /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
156	155	ex 450	. . . . . . . . . 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 /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
157	22, 156	ralrimi 2957	. . . . . . . . 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 /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
158		unieq 4444	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> U. x = U. ( g ` y ) )
159	158	sseq2d 3633	. . . . . . . . . . . 12 |- ( x = ( g ` y ) -> ( A C_ U. x <-> A C_ U. ( g ` y ) ) )
160		esumeq1 30096	. . . . . . . . . . . . 13 |- ( x = ( g ` y ) -> Σ* w e. x ( R ` w ) = Σ* w e. ( g ` y ) ( R ` w ) )
161	160	breq1d 4663	. . . . . . . . . . . 12 |- ( x = ( g ` y ) -> (Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) <-> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
162	159, 161	anbi12d 747	. . . . . . . . . . 11 |- ( x = ( g ` y ) -> ( ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) <-> ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
163	162	ac6sg 9310	. . . . . . . . . 10 |- ( X e. _V -> ( A. y e. X E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) ) )
164	163	imp 445	. . . . . . . . 9 |- ( ( X e. _V /\ A. y e. X E. x e. { z e. ~P dom R | z ~<_ om } ( A C_ U. x /\ Σ* w e. x ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> E. g ( g : X --> { z e. ~P dom R | z ~<_ om } /\ A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
165	12, 157, 164	syl2anc 693	. . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
166	9	ad2antrr 762	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ph )
167	39	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. y e. X A C_ U. dom R )
168		iunss 4561	. . . . . . . . . . . . . . . . . 18 |- ( U_ y e. X A C_ U. dom R <-> A. y e. X A C_ U. dom R )
169	167, 168	sylibr 224	. . . . . . . . . . . . . . . . 17 |- ( ph -> U_ y e. X A C_ U. dom R )
170	44	ralrimiva 2966	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. y e. X A e. _V )
171		iunexg 7143	. . . . . . . . . . . . . . . . . . 19 |- ( ( X e. _V /\ A. y e. X A e. _V ) -> U_ y e. X A e. _V )
172	11, 170, 171	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U_ y e. X A e. _V )
173		elpwg 4166	. . . . . . . . . . . . . . . . . 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 ) )
174	172, 173	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( U_ y e. X A e. ~P U. dom R <-> U_ y e. X A C_ U. dom R ) )
175	169, 174	mpbird 247	. . . . . . . . . . . . . . . 16 |- ( ph -> U_ y e. X A e. ~P U. dom R )
176	32, 175	ffvelrnd 6360	. . . . . . . . . . . . . . 15 |- ( ph -> ( M ` U_ y e. X A ) e. ( 0 [,] +oo ) )
177	107, 176	sseldi 3601	. . . . . . . . . . . . . 14 |- ( ph -> ( M ` U_ y e. X A ) e. RR* )
178	166, 177	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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) e. RR* )
179		simplr 792	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
180	25	ad4antr 768	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X e. _V )
181		fex 6490	. . . . . . . . . . . . . . . . 17 |- ( ( g : X --> { z e. ~P dom R | z ~<_ om } /\ X e. _V ) -> g e. _V )
182	179, 180, 181	syl2anc 693	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g e. _V )
183		rnexg 7098	. . . . . . . . . . . . . . . 16 |- ( g e. _V -> ran g e. _V )
184		uniexg 6955	. . . . . . . . . . . . . . . 16 |- ( ran g e. _V -> U. ran g e. _V )
185	182, 183, 184	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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. _V )
186		simp-5l 808	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ph )
187	27	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> R : Q --> ( 0 [,] +oo ) )
188		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ { z e. ~P dom R | z ~<_ om } )
189		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { z e. ~P dom R | z ~<_ om } C_ ~P dom R
190	188, 189	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
191	190	unissd 4462	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ U. ~P dom R )
192		unipw 4918	. . . . . . . . . . . . . . . . . . . . . 22 |- U. ~P dom R = dom R
193	191, 192	syl6sseq 3651	. . . . . . . . . . . . . . . . . . . . 21 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
194	193	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ dom R )
195	36	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> dom R = Q )
196	194, 195	sseqtrd 3641	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U. ran g C_ Q )
197	196	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> c e. Q )
198	187, 197	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ c e. U. ran g ) -> ( R ` c ) e. ( 0 [,] +oo ) )
199	198	ralrimiva 2966	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
200	186, 179, 199	syl2anc 693	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
201		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ c U. ran g
202	201	esumcl 30092	. . . . . . . . . . . . . . 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 ) )
203	185, 200, 202	syl2anc 693	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* c e. U. ran g ( R ` c ) e. ( 0 [,] +oo ) )
204	107, 203	sseldi 3601	. . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* c e. U. ran g ( R ` c ) e. RR* )
205		simp-5r 809	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( M ` A ) e. RR )
206	205	rexrd 10089	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( M ` A ) e. RR* )
207		simpllr 799	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR+ )
208	207	rpxrd 11873	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR* )
209	206, 208	xaddcld 12131	. . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> (Σ* y e. X ( M ` A ) +e e ) e. RR* )
210	188	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ran g C_ { z e. ~P dom R | z ~<_ om } )
211		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . 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 )
212	189, 211	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> ran g C_ ~P dom R )
213		sspwuni 4611	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ran g C_ ~P dom R <-> U. ran g C_ dom R )
214	212, 213	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> U. ran g C_ dom R )
215	210, 214	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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g C_ dom R )
216		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g : X --> { z e. ~P dom R | z ~<_ om } -> g Fn X )
217	216	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> g Fn X )
218	166, 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X ~<_ om )
219		fnct 9359	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g Fn X /\ X ~<_ om ) -> g ~<_ om )
220		rnct 9347	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( g ~<_ om -> ran g ~<_ om )
221	219, 220	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( g Fn X /\ X ~<_ om ) -> ran g ~<_ om )
222		dfss3 3592	. . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
223	222	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . 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 } )
224		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = w -> ( z ~<_ om <-> w ~<_ om ) )
225	224	elrab 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. { z e. ~P dom R | z ~<_ om } <-> ( w e. ~P dom R /\ w ~<_ om ) )
226	225	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( w e. { z e. ~P dom R | z ~<_ om } -> w ~<_ om )
227	226	ralimi 2952	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. w e. ran g w e. { z e. ~P dom R | z ~<_ om } -> A. w e. ran g w ~<_ om )
228	223, 227	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ran g C_ { z e. ~P dom R | z ~<_ om } -> A. w e. ran g w ~<_ om )
229		unictb 9397	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ran g ~<_ om /\ A. w e. ran g w ~<_ om ) -> U. ran g ~<_ om )
230	221, 228, 229	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( g Fn X /\ X ~<_ om ) /\ ran g C_ { z e. ~P dom R | z ~<_ om } ) -> U. ran g ~<_ om )
231	217, 218, 210, 230	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g ~<_ om )
232		ctex 7970	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g ~<_ om -> U. ran g e. _V )
233		elpwg 4166	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. ran g e. _V -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
234	231, 232, 233	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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( U. ran g e. ~P dom R <-> U. ran g C_ dom R ) )
235	215, 234	mpbird 247	. . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. ~P dom R )
236		simpl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A C_ U. ( g ` y ) )
237	236	ralimi 2952	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A. y e. X A C_ U. ( g ` y ) )
238		fvssunirn 6217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( g ` y ) C_ U. ran g
239	238	unissi 4461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U. ( g ` y ) C_ U. U. ran g
240		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A C_ U. ( g ` y ) /\ U. ( g ` y ) C_ U. U. ran g ) -> A C_ U. U. ran g )
241	239, 240	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A C_ U. ( g ` y ) -> A C_ U. U. ran g )
242	241	ralimi 2952	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. y e. X A C_ U. ( g ` y ) -> A. y e. X A C_ U. U. ran g )
243		iunss 4561	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( U_ y e. X A C_ U. U. ran g <-> A. y e. X A C_ U. U. ran g )
244	242, 243	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. y e. X A C_ U. ( g ` y ) -> U_ y e. X A C_ U. U. ran g )
245	237, 244	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> U_ y e. X A C_ U. U. ran g )
246	245	adantl 482	. . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U_ y e. X A C_ U. U. ran g )
247	235, 246, 231	jca32 558	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( U. ran g e. ~P dom R /\ ( U_ y e. X A C_ U. U. ran g /\ U. ran g ~<_ om ) ) )
248		unieq 4444	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = U. ran g -> U. z = U. U. ran g )
249	248	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( U_ y e. X A C_ U. z <-> U_ y e. X A C_ U. U. ran g ) )
250		breq1 4656	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = U. ran g -> ( z ~<_ om <-> U. ran g ~<_ om ) )
251	249, 250	anbi12d 747	. . . . . . . . . . . . . . . . . . . 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 ) ) )
252	251	elrab 3363	. . . . . . . . . . . . . . . . . . 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 ) ) )
253	247, 252	sylibr 224	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> U. ran g e. { z e. ~P dom R | ( U_ y e. X A C_ U. z /\ z ~<_ om ) } )
254		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( c = w -> ( R ` c ) = ( R ` w ) )
255	254	cbvesumv 30105	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) = Σ* w e. U. ran g ( R ` w )
256		esumeq1 30096	. . . . . . . . . . . . . . . . . . . 20 |- ( x = U. ran g -> Σ* w e. x ( R ` w ) = Σ* w e. U. ran g ( R ` w ) )
257	256	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 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 ) ) )
258	257	rspcev 3309	. . . . . . . . . . . . . . . . . 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 ) )
259	253, 255, 258	sylancl 694	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> 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		esumex 30091	. . . . . . . . . . . . . . . . . 18 |- Σ* c e. U. ran g ( R ` c ) e. _V
261		eqid 2622	. . . . . . . . . . . . . . . . . . 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 ) )
262	261	elrnmpt 5372	. . . . . . . . . . . . . . . . . 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 ) ) )
263	260, 262	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 ) )
264	259, 263	sylibr 224	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* 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 ) ) )
265	112	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> < Or ( 0 [,] +oo ) )
266		omscl 30357	. . . . . . . . . . . . . . . . . . . 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 ) )
267	26, 27, 175, 266	syl3anc 1326	. . . . . . . . . . . . . . . . . . 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 ) )
268		xrge0infss 29525	. . . . . . . . . . . . . . . . . . 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 ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> 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 ) ) u < t ) ) )
269	267, 268	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 ) ) -. t < e /\ A. t e. ( 0 [,] +oo ) ( e < t -> 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 ) ) u < t ) ) )
270	265, 269	inflb 8395	. . . . . . . . . . . . . . . . 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 ) ) -> -. Σ* c e. U. ran g ( R ` c ) < inf ( 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 ) , < ) ) )
271	29	fveq1i 6192	. . . . . . . . . . . . . . . . . . . 20 |- ( M ` U_ y e. X A ) = ( (toOMeas ` R ) ` U_ y e. X A )
272	169, 37	sseqtrd 3641	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U_ y e. X A C_ U. Q )
273		omsfval 30356	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ U_ y e. X A C_ U. Q ) -> ( (toOMeas ` R ) ` U_ y e. X A ) = inf ( 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 ) , < ) )
274	26, 27, 272, 273	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( (toOMeas ` R ) ` U_ y e. X A ) = inf ( 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	271, 274	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M ` U_ y e. X A ) = inf ( 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	275	breq2d 4665	. . . . . . . . . . . . . . . . . 18 |- ( ph -> (Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> Σ* c e. U. ran g ( R ` c ) < inf ( 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	notbid 308	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> -. Σ* c e. U. ran g ( R ` c ) < inf ( 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 ) , < ) ) )
278	270, 277	sylibrd 249	. . . . . . . . . . . . . . . 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 ) ) -> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) ) )
279	166, 264, 278	sylc 65	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
280		biid 251	. . . . . . . . . . . . . . 15 |- ( -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) <-> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
281	279, 280	sylib 208	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> -. Σ* c e. U. ran g ( R ` c ) < ( M ` U_ y e. X A ) )
282		xrlenlt 10103	. . . . . . . . . . . . . . 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 ) ) )
283	178, 204, 282	syl2anc 693	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( ( 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	281, 283	mpbird 247	. . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ Σ* c e. U. ran g ( R ` c ) )
285		nfv 1843	. . . . . . . . . . . . . . . . . . 19 |- F/ y g : X --> { z e. ~P dom R | z ~<_ om }
286	22, 285	nfan 1828	. . . . . . . . . . . . . . . . . 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 } )
287		nfra1 2941	. . . . . . . . . . . . . . . . . 18 |- F/ y A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
288	286, 287	nfan 1828	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
289		simp-6l 810	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ph )
290		simpllr 799	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
291		simpr 477	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> y e. X )
292	27	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> R : Q --> ( 0 [,] +oo ) )
293		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
294		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> y e. X )
295	293, 294	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . 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 } )
296	189, 295	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) e. ~P dom R )
297	296	elpwid 4170	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ dom R )
298	292, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> dom R = Q )
299	297, 298	sseqtrd 3641	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( g ` y ) C_ Q )
300		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. ( g ` y ) )
301	299, 300	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> w e. Q )
302	292, 301	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) /\ w e. ( g ` y ) ) -> ( R ` w ) e. ( 0 [,] +oo ) )
303	302	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) -> A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
304		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( g ` y ) e. _V
305		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ w ( g ` y )
306	305	esumcl 30092	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( g ` y ) e. _V /\ A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) ) -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
307	304, 306	mpan 706	. . . . . . . . . . . . . . . . . . . 20 |- ( A. w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
308	303, 307	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
309	289, 290, 291, 308	syl21anc 1325	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
310	309	ex 450	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( y e. X -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) ) )
311	288, 310	ralrimi 2957	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
312	14	esumcl 30092	. . . . . . . . . . . . . . . 16 |- ( ( X e. _V /\ A. y e. X Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) ) -> Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
313	180, 311, 312	syl2anc 693	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
314	107, 313	sseldi 3601	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) e. RR* )
315		nfv 1843	. . . . . . . . . . . . . . . . . . 19 |- F/ w ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } )
316		simpr 477	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
317		fniunfv 6505	. . . . . . . . . . . . . . . . . . . 20 |- ( g Fn X -> U_ y e. X ( g ` y ) = U. ran g )
318	316, 216, 317	3syl 18	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> U_ y e. X ( g ` y ) = U. ran g )
319	315, 318	esumeq1d 30097	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> Σ* w e. U_ y e. X ( g ` y ) ( R ` w ) = Σ* w e. U. ran g ( R ` w ) )
320	11	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> X e. _V )
321	304	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) /\ y e. X ) -> ( g ` y ) e. _V )
322	320, 321, 302	esumiun 30156	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> Σ* w e. U_ y e. X ( g ` y ) ( R ` w ) <_ Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) )
323	319, 322	eqbrtrrd 4677	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ g : X --> { z e. ~P dom R | z ~<_ om } ) -> Σ* w e. U. ran g ( R ` w ) <_ Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) )
324	9, 323	sylan 488	. . . . . . . . . . . . . . . 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 } ) -> Σ* w e. U. ran g ( R ` w ) <_ Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) )
325	324	adantr 481	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* w e. U. ran g ( R ` w ) <_ Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) )
326	255, 325	syl5eqbr 4688	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* c e. U. ran g ( R ` c ) <_ Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) )
327	289, 291, 48	syl2anc 693	. . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
328		simplll 798	. . . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) )
329	328, 291, 75	syl2anc 693	. . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
330	327, 329	xrge0addcld 29527	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
331	330	ex 450	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( y e. X -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) ) )
332	288, 331	ralrimi 2957	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
333	14	esumcl 30092	. . . . . . . . . . . . . . . . 17 |- ( ( X e. _V /\ A. y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) ) -> Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
334	180, 332, 333	syl2anc 693	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. ( 0 [,] +oo ) )
335	107, 334	sseldi 3601	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* )
336	218, 10	syl 17	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> X e. _V )
337		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( ph /\ Σ* y e. X ( M ` A ) e. RR ) )
338		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> y e. X )
339	337, 338, 51	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( M ` A ) e. RR )
340	339	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 } ) /\ y e. X ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( M ` A ) e. RR )
341	67	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
342	341	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 } ) /\ y e. X ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR )
343		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
344	343	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 } ) /\ y e. X ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) )
345	68	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) -> (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) <-> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
346	345	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( M ` A ) e. RR /\ ( e / ( 2 ^ ( f ` y ) ) ) e. RR ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
347	340, 342, 344, 346	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 } ) /\ y e. X ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
348	347	ex 450	. . . . . . . . . . . . . . . . . . . . . . 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 } ) /\ y e. X ) -> (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
349	337	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ph )
350		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> g : X --> { z e. ~P dom R | z ~<_ om } )
351	349, 350, 338, 308	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> Σ* w e. ( g ` y ) ( R ` w ) e. ( 0 [,] +oo ) )
352	107, 351	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> Σ* w e. ( g ` y ) ( R ` w ) e. RR* )
353	339	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( M ` A ) e. RR* )
354	341	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) e. RR* )
355	353, 354	xaddcld 12131	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 } ) /\ y e. X ) -> ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* )
356		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( (Σ* w e. ( g ` y ) ( R ` w ) e. RR* /\ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) e. RR* ) -> (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
357	352, 355, 356	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 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 } ) /\ y e. X ) -> (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
358	348, 357	syld 47	. . . . . . . . . . . . . . . . . . . . . 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 } ) /\ y e. X ) -> (Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
359	358	adantld 483	. . . . . . . . . . . . . . . . . . . . 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 } ) /\ y e. X ) -> ( ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
360	359	ex 450	. . . . . . . . . . . . . . . . . . . 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 } ) -> ( y e. X -> ( ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) )
361	286, 360	ralrimi 2957	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
362		ralim 2948	. . . . . . . . . . . . . . . . . . 19 |- ( A. y e. X ( ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> ( A. y e. X ( A C_ U. ( g ` y ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A. y e. X Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
363	361, 362	syl 17	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) -> A. y e. X Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) ) )
364	363	imp 445	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
365	364	r19.21bi 2932	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> Σ* w e. ( g ` y ) ( R ` w ) <_ ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
366	288, 14, 336, 309, 330, 365	esumlef 30124	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) <_ Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) )
367	166, 48	sylan 488	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) /\ y e. X ) -> ( M ` A ) e. ( 0 [,] +oo ) )
368	288, 14, 336, 367, 329	esumaddf 30123	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) = (Σ* y e. X ( M ` A ) +eΣ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) )
369	329	ex 450	. . . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( y e. X -> ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) ) )
370	288, 369	ralrimi 2957	. . . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
371	14	esumcl 30092	. . . . . . . . . . . . . . . . . . 19 |- ( ( X e. _V /\ A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
372	180, 370, 371	syl2anc 693	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
373	107, 372	sseldi 3601	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. RR* )
374		simp-4r 807	. . . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> f : X -1-1-> NN )
375		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . 24 |- f e. _V
376	375	rnex 7100	. . . . . . . . . . . . . . . . . . . . . . 23 |- ran f e. _V
377	376	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ran f e. _V )
378		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f : X --> NN -> ran f C_ NN )
379	60, 378	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ f : X -1-1-> NN ) -> ran f C_ NN )
380	379	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ran f C_ NN )
381	380	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> z e. NN )
382	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> 2 e. RR+ )
383		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. NN )
384	383	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> z e. ZZ )
385	382, 384	rpexpcld 13032	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 2 ^ z ) e. RR+ )
386	385	rpreccld 11882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. RR+ )
387	73, 386	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
388	387	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
389	381, 388	syldan 487	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ z e. ran f ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
390	389	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
391		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ z ran f
392	391	esumcl 30092	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ran f e. _V /\ A. z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
393	377, 390, 392	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) e. ( 0 [,] +oo ) )
394	107, 393	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) e. RR* )
395		1re 10039	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. RR
396		rexr 10085	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 e. RR -> 1 e. RR* )
397	395, 396	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR*
398	397	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> 1 e. RR* )
399	73	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22 |- ( e e. RR+ -> e e. ( 0 [,] +oo ) )
400	399	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,] +oo ) )
401		elxrge0 12281	. . . . . . . . . . . . . . . . . . . . 21 |- ( e e. ( 0 [,] +oo ) <-> ( e e. RR* /\ 0 <_ e ) )
402	400, 401	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e e. RR* /\ 0 <_ e ) )
403		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ z ( ph /\ f : X -1-1-> NN )
404		nnex 11026	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN e. _V
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f : X -1-1-> NN ) -> NN e. _V )
406	403, 405, 387, 379	esummono 30116	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) <_ Σ* z e. NN ( 1 / ( 2 ^ z ) ) )
407		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = w -> ( 2 ^ z ) = ( 2 ^ w ) )
408	407	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = w -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ w ) ) )
409		ioossico 12262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 0 (,) +oo ) C_ ( 0 [,) +oo )
410	71, 409	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- RR+ C_ ( 0 [,) +oo )
411	410, 386	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( 1 / ( 2 ^ z ) ) e. ( 0 [,) +oo ) )
412		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. NN -> ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) )
413		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( z e. NN /\ w = z ) -> w = z )
414	413	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( z e. NN /\ w = z ) -> ( 2 ^ w ) = ( 2 ^ z ) )
415	414	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( z e. NN /\ w = z ) -> ( 1 / ( 2 ^ w ) ) = ( 1 / ( 2 ^ z ) ) )
416		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. NN -> z e. NN )
417		ovexd 6680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. NN -> ( 1 / ( 2 ^ z ) ) e. _V )
418	412, 415, 416, 417	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z e. NN -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
419	418	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ z e. NN ) -> ( ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ` z ) = ( 1 / ( 2 ^ z ) ) )
420		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 1 e. CC
421		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) = ( w e. NN |-> ( 1 / ( 2 ^ w ) ) )
422	421	geo2lim 14606	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 1 e. CC -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
423	420, 422	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1
424	423	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> seq 1 ( + , ( w e. NN |-> ( 1 / ( 2 ^ w ) ) ) ) ~~> 1 )
425	395	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> 1 e. RR )
426	408, 411, 419, 424, 425	esumcvgsum 30150	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* z e. NN ( 1 / ( 2 ^ z ) ) = sum_ z e. NN ( 1 / ( 2 ^ z ) ) )
427		geoihalfsum 14614	. . . . . . . . . . . . . . . . . . . . . . 23 |- sum_ z e. NN ( 1 / ( 2 ^ z ) ) = 1
428	426, 427	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* z e. NN ( 1 / ( 2 ^ z ) ) = 1 )
429	406, 428	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
430	429	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 )
431		xlemul2a 12119	. . . . . . . . . . . . . . . . . . . 20 |- ( ( (Σ* z e. ran f ( 1 / ( 2 ^ z ) ) e. RR* /\ 1 e. RR* /\ ( e e. RR* /\ 0 <_ e ) ) /\ Σ* z e. ran f ( 1 / ( 2 ^ z ) ) <_ 1 ) -> ( e xeΣ* z e. ran f ( 1 / ( 2 ^ z ) ) ) <_ ( e xe 1 ) )
432	394, 398, 402, 430, 431	syl31anc 1329	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e xeΣ* z e. ran f ( 1 / ( 2 ^ z ) ) ) <_ ( e xe 1 ) )
433	13, 19	nfan 1828	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ y ( ph /\ f : X -1-1-> NN )
434	433, 21	nfan 1828	. . . . . . . . . . . . . . . . . . . . 21 |- F/ y ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ )
435	78	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> e e. CC )
436	80	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
437	436	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) e. CC )
438		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 2 e. CC
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 e. CC )
440		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 2 =/= 0
441	440	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 2 =/= 0 )
442	439, 441, 62	expne0d 13014	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
443	442	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 2 ^ ( f ` y ) ) =/= 0 )
444	435, 437, 443	divrecd 10804	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
445		1rp 11836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 1 e. RR+
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> 1 e. RR+ )
447	446, 63	rpdivcld 11889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR+ )
448	54, 447	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
449	448	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR )
450		rexmul 12101	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( e e. RR /\ ( 1 / ( 2 ^ ( f ` y ) ) ) e. RR ) -> ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
451	78, 449, 450	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e x. ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
452	444, 451	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( e / ( 2 ^ ( f ` y ) ) ) = ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
453	452	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> A. y e. X ( e / ( 2 ^ ( f ` y ) ) ) = ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
454	434, 453	esumeq2d 30099	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) = Σ* y e. X ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
455	11	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> X e. _V )
456	73, 447	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
457	456	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) /\ y e. X ) -> ( 1 / ( 2 ^ ( f ` y ) ) ) e. ( 0 [,] +oo ) )
458	410	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f : X -1-1-> NN ) -> RR+ C_ ( 0 [,) +oo ) )
459	458	sselda 3603	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. ( 0 [,) +oo ) )
460	455, 457, 459	esummulc2 30144	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e xeΣ* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) ) = Σ* y e. X ( e xe ( 1 / ( 2 ^ ( f ` y ) ) ) ) )
461		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ y ( 1 / ( 2 ^ z ) )
462		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( f ` y ) -> ( 2 ^ z ) = ( 2 ^ ( f ` y ) ) )
463	462	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = ( f ` y ) -> ( 1 / ( 2 ^ z ) ) = ( 1 / ( 2 ^ ( f ` y ) ) ) )
464	11	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> X e. _V )
465	58	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN -> Fun `' f )
466	59	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f : X -1-1-> NN -> f = ( y e. X |-> ( f ` y ) ) )
467	466	cnveqd 5298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f : X -1-1-> NN -> `' f = `' ( y e. X |-> ( f ` y ) ) )
468	467	funeqd 5910	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : X -1-1-> NN -> ( Fun `' f <-> Fun `' ( y e. X |-> ( f ` y ) ) ) )
469	465, 468	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X -1-1-> NN -> Fun `' ( y e. X |-> ( f ` y ) ) )
470	469	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> Fun `' ( y e. X |-> ( f ` y ) ) )
471	461, 433, 14, 463, 464, 470, 456, 61	esumc 30113	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = Σ* z e. { x | E. y e. X x = ( f ` y ) } ( 1 / ( 2 ^ z ) ) )
472		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : X --> NN -> f Fn X )
473		fnrnfv 6242	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f Fn X -> ran f = { x | E. y e. X x = ( f ` y ) } )
474	60, 472, 473	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ f : X -1-1-> NN ) -> ran f = { x | E. y e. X x = ( f ` y ) } )
475	403, 474	esumeq1d 30097	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* z e. ran f ( 1 / ( 2 ^ z ) ) = Σ* z e. { x | E. y e. X x = ( f ` y ) } ( 1 / ( 2 ^ z ) ) )
476	471, 475	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ f : X -1-1-> NN ) -> Σ* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = Σ* z e. ran f ( 1 / ( 2 ^ z ) ) )
477	476	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) = Σ* z e. ran f ( 1 / ( 2 ^ z ) ) )
478	477	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e xeΣ* y e. X ( 1 / ( 2 ^ ( f ` y ) ) ) ) = ( e xeΣ* z e. ran f ( 1 / ( 2 ^ z ) ) ) )
479	454, 460, 478	3eqtr2rd 2663	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e xeΣ* z e. ran f ( 1 / ( 2 ^ z ) ) ) = Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) )
480	402	simpld 475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> e e. RR* )
481		xmulid1 12109	. . . . . . . . . . . . . . . . . . . 20 |- ( e e. RR* -> ( e xe 1 ) = e )
482	480, 481	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( e xe 1 ) = e )
483	432, 479, 482	3brtr3d 4684	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e )
484	166, 374, 207, 483	syl21anc 1325	. . . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e )
485		xleadd2a 12084	. . . . . . . . . . . . . . . . 17 |- ( ( (Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) e. RR* /\ e e. RR* /\ Σ* y e. X ( M ` A ) e. RR* ) /\ Σ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) <_ e ) -> (Σ* y e. X ( M ` A ) +eΣ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) <_ (Σ* y e. X ( M ` A ) +e e ) )
486	373, 208, 206, 484, 485	syl31anc 1329	. . . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> (Σ* y e. X ( M ` A ) +eΣ* y e. X ( e / ( 2 ^ ( f ` y ) ) ) ) <_ (Σ* y e. X ( M ` A ) +e e ) )
487	368, 486	eqbrtrd 4675	. . . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. X ( ( M ` A ) +e ( e / ( 2 ^ ( f ` y ) ) ) ) <_ (Σ* y e. X ( M ` A ) +e e ) )
488	314, 335, 209, 366, 487	xrletrd 11993	. . . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* y e. XΣ* w e. ( g ` y ) ( R ` w ) <_ (Σ* y e. X ( M ` A ) +e e ) )
489	204, 314, 209, 326, 488	xrletrd 11993	. . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> Σ* c e. U. ran g ( R ` c ) <_ (Σ* y e. X ( M ` A ) +e e ) )
490	178, 204, 209, 284, 489	xrletrd 11993	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) +e e ) )
491	207	rpred 11872	. . . . . . . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> e e. RR )
492		rexadd 12063	. . . . . . . . . . . . 13 |- ( (Σ* y e. X ( M ` A ) e. RR /\ e e. RR ) -> (Σ* y e. X ( M ` A ) +e e ) = (Σ* y e. X ( M ` A ) + e ) )
493	205, 491, 492	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> (Σ* y e. X ( M ` A ) +e e ) = (Σ* y e. X ( M ` A ) + e ) )
494	490, 493	breqtrd 4679	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) )
495	494	anasss 679	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) )
496	495	ex 450	. . . . . . . . 9 |- ( ( ( ( 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) ) )
497	496	exlimdv 1861	. . . . . . . 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 ) /\ Σ* w e. ( g ` y ) ( R ` w ) < ( ( M ` A ) + ( e / ( 2 ^ ( f ` y ) ) ) ) ) ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) ) )
498	165, 497	mpd 15	. . . . . . 7 |- ( ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) /\ e e. RR+ ) -> ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) )
499	498	ralrimiva 2966	. . . . . 6 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> A. e e. RR+ ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) )
500		xralrple 12036	. . . . . . . 8 |- ( ( ( M ` U_ y e. X A ) e. RR* /\ Σ* y e. X ( M ` A ) e. RR ) -> ( ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) ) )
501	177, 500	sylan 488	. . . . . . 7 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> ( ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) ) )
502	501	adantr 481	. . . . . 6 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> ( ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) <-> A. e e. RR+ ( M ` U_ y e. X A ) <_ (Σ* y e. X ( M ` A ) + e ) ) )
503	499, 502	mpbird 247	. . . . 5 |- ( ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) /\ f : X -1-1-> NN ) -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )
504	503	ex 450	. . . 4 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> ( f : X -1-1-> NN -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) ) )
505	504	exlimdv 1861	. . 3 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> ( E. f f : X -1-1-> NN -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) ) )
506	8, 505	mpd 15	. 2 |- ( ( ph /\ Σ* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )
507	177	adantr 481	. . . 4 |- ( ( ph /\ -. Σ* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) e. RR* )
508		pnfge 11964	. . . 4 |- ( ( M ` U_ y e. X A ) e. RR* -> ( M ` U_ y e. X A ) <_ +oo )
509	507, 508	syl 17	. . 3 |- ( ( ph /\ -. Σ* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ +oo )
510	48	ralrimiva 2966	. . . . 5 |- ( ph -> A. y e. X ( M ` A ) e. ( 0 [,] +oo ) )
511	14	esumcl 30092	. . . . 5 |- ( ( X e. _V /\ A. y e. X ( M ` A ) e. ( 0 [,] +oo ) ) -> Σ* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
512	11, 510, 511	syl2anc 693	. . . 4 |- ( ph -> Σ* y e. X ( M ` A ) e. ( 0 [,] +oo ) )
513		xrge0nre 12277	. . . 4 |- ( (Σ* y e. X ( M ` A ) e. ( 0 [,] +oo ) /\ -. Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) = +oo )
514	512, 513	sylan 488	. . 3 |- ( ( ph /\ -. Σ* y e. X ( M ` A ) e. RR ) -> Σ* y e. X ( M ` A ) = +oo )
515	509, 514	breqtrrd 4681	. 2 |- ( ( ph /\ -. Σ* y e. X ( M ` A ) e. RR ) -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )
516	506, 515	pm2.61dan 832	1 |- ( ph -> ( M ` U_ y e. X A ) <_ Σ* y e. X ( M ` A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   ~Pcpw 4158   U.cuni 4436   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   `'ccnv 5113   dom cdm 5114   ran crn 5115   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   ` cfv 5888  (class class class)co 6650   omcom 7065   ~~ cen 7952   ~<_ cdom 7953  infcinf 8347   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   / cdiv 10684   NNcn 11020   2c2 11070   ZZcz 11377   RR+crp 11832   +ecxad 11944   xecxmu 11945   (,)cioo 12175   [,)cico 12177   [,]cicc 12178   seqcseq 12801   ^cexp 12860   ~~> cli 14215   sum_csu 14416  Σ^*cesum 30089  toOMeascoms 30353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-reg 8497  ax-inf2 8538  ax-cc 9257  ax-ac2 9285  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-r1 8627  df-rank 8628  df-card 8765  df-acn 8768  df-ac 8939  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-pi 14803  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-ordt 16161  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-ps 17200  df-tsr 17201  df-plusf 17241  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-subrg 18778  df-abv 18817  df-lmod 18865  df-scaf 18866  df-sra 19172  df-rgmod 19173  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-tmd 21876  df-tgp 21877  df-tsms 21930  df-trg 21963  df-xms 22125  df-ms 22126  df-tms 22127  df-nm 22387  df-ngp 22388  df-nrg 22390  df-nlm 22391  df-ii 22680  df-cncf 22681  df-limc 23630  df-dv 23631  df-log 24303  df-esum 30090  df-oms 30354

This theorem is referenced by:  omsmeas  30385