omssubadd

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) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	oms.m	$⊢ M = toOMeas (R)$
	oms.o	$⊢ φ \to Q \in V$
	oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
	omssubadd.a	$⊢ (φ \land y \in X) \to A \subseteq ⋃ Q$
	omssubadd.b	$⊢ φ \to X ≼ ω$
Assertion	omssubadd	$⊢ φ \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A)$

Proof

Step	Hyp	Ref	Expression
1		oms.m	$⊢ M = toOMeas (R)$
2		oms.o	$⊢ φ \to Q \in V$
3		oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
4		omssubadd.a	$⊢ (φ \land y \in X) \to A \subseteq ⋃ Q$
5		omssubadd.b	$⊢ φ \to X ≼ ω$
6		nnenom	$⊢ ℕ \approx ω$
7		domen2	$⊢ ℕ \approx ω \to (X ≼ ℕ \leftrightarrow X ≼ ω)$
8	6 7	ax-mp	$⊢ X ≼ ℕ \leftrightarrow X ≼ ω$
9	5 8	sylibr	$⊢ φ \to X ≼ ℕ$
10		brdomi	$⊢ X ≼ ℕ \to \exists f f : X \underset{1-1}{⟶} ℕ$
11	9 10	syl	$⊢ φ \to \exists f f : X \underset{1-1}{⟶} ℕ$
12	11	adantr	$⊢ (φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \to \exists f f : X \underset{1-1}{⟶} ℕ$
13		simplll	$⊢ (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to φ$
14		ctex	$⊢ X ≼ ω \to X \in V$
15	5 14	syl	$⊢ φ \to X \in V$
16	13 15	syl	$⊢ (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to X \in V$
17	3 2	fexd	$⊢ φ \to R \in V$
18		dmexg	$⊢ R \in V \to dom R \in V$
19		pwexg	$⊢ dom R \in V \to 𝒫 dom R \in V$
20	17 18 19	3syl	$⊢ φ \to 𝒫 dom R \in V$
21		rabexg	$⊢ 𝒫 dom R \in V \to \{z \in 𝒫 dom R \| z ≼ ω\} \in V$
22	20 21	syl	$⊢ φ \to \{z \in 𝒫 dom R \| z ≼ ω\} \in V$
23	22	ad3antrrr	$⊢ (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \{z \in 𝒫 dom R \| z ≼ ω\} \in V$
24		nfv	$⊢ Ⅎ y φ$
25		nfcv	$⊢ \underline{Ⅎ} y X$
26	25	nfesum1	$⊢ \underline{Ⅎ} y \underset{y \in X}{\sum^{*}} M (A)$
27	26	nfel1	$⊢ Ⅎ y \underset{y \in X}{\sum^{*}} M (A) \in ℝ$
28	24 27	nfan	$⊢ Ⅎ y (φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ)$
29		nfv	$⊢ Ⅎ y f : X \underset{1-1}{⟶} ℕ$
30	28 29	nfan	$⊢ Ⅎ y ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ)$
31		nfv	$⊢ Ⅎ y e \in ℝ^{+}$
32	30 31	nfan	$⊢ Ⅎ y (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+})$
33	13	adantr	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to φ$
34		simpr	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to y \in X$
35	15	adantr	$⊢ (φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \to X \in V$
36		omsf	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
37	1	feq1i	$⊢ M : 𝒫 ⋃ dom R ⟶ [0, +∞] \leftrightarrow toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
38	36 37	sylibr	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
39	2 3 38	syl2anc	$⊢ φ \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
40	39	adantr	$⊢ (φ \land y \in X) \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
41	2	uniexd	$⊢ φ \to ⋃ Q \in V$
42	41	adantr	$⊢ (φ \land y \in X) \to ⋃ Q \in V$
43	42 4	ssexd	$⊢ (φ \land y \in X) \to A \in V$
44	3	fdmd	$⊢ φ \to dom R = Q$
45	44	unieqd	$⊢ φ \to ⋃ dom R = ⋃ Q$
46	45	adantr	$⊢ (φ \land y \in X) \to ⋃ dom R = ⋃ Q$
47	4 46	sseqtrrd	$⊢ (φ \land y \in X) \to A \subseteq ⋃ dom R$
48	43 47	elpwd	$⊢ (φ \land y \in X) \to A \in 𝒫 ⋃ dom R$
49	40 48	ffvelcdmd	$⊢ (φ \land y \in X) \to M (A) \in [0, +∞]$
50	49	adantlr	$⊢ ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land y \in X) \to M (A) \in [0, +∞]$
51		simpr	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to \underset{y \in X}{\sum^{}} M (A) \in ℝ$
52	28 35 50 51	esumcvgre	$⊢ ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land y \in X) \to M (A) \in ℝ$
53	52	ad4ant14	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) \in ℝ$
54		simplr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ^{+}$
55		2rp	$⊢ 2 \in ℝ^{+}$
56	55	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \in ℝ^{+}$
57		f1f	$⊢ f : X \underset{1-1}{⟶} ℕ \to f : X ⟶ ℕ$
58	57	adantl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to f : X ⟶ ℕ$
59	58	ffvelcdmda	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to f (y) \in ℕ$
60	59	nnzd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to f (y) \in ℤ$
61	56 60	rpexpcld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \in ℝ^{+}$
62	61	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℝ^{+}$
63	54 62	rpdivcld	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ^{+}$
64	63	rpred	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ$
65	64	adantl3r	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ$
66	53 65	rexaddd	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) = M (A) + (\frac{e}{2^{f (y)}})$
67	49	ad5ant15	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) \in [0, +∞]$
68		dfrp2	$⊢ ℝ^{+} = (0, +∞)$
69		ioossicc	$⊢ (0, +∞) \subseteq [0, +∞]$
70	68 69	eqsstri	$⊢ ℝ^{+} \subseteq [0, +∞]$
71	70 63	sselid	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in [0, +∞]$
72	71	adantl3r	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in [0, +∞]$
73	67 72	xrge0addcld	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in [0, +∞]$
74	66 73	eqeltrrd	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) + (\frac{e}{2^{f (y)}}) \in [0, +∞]$
75	1	fveq1i	$⊢ M (A) = toOMeas (R) (A)$
76	2	adantr	$⊢ (φ \land y \in X) \to Q \in V$
77	3	adantr	$⊢ (φ \land y \in X) \to R : Q ⟶ [0, +∞]$
78		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \subseteq ⋃ Q) \to toOMeas (R) (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
79	76 77 4 78	syl3anc	$⊢ (φ \land y \in X) \to toOMeas (R) (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
80	75 79	eqtrid	$⊢ (φ \land y \in X) \to M (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
81	80	ad5ant15	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) = inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <)$
82	54	rpred	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ$
83	82	adantl3r	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ$
84	61	rpred	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \in ℝ$
85	84	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℝ$
86	85	adantl3r	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℝ$
87		simplr	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ^{+}$
88	87	rpgt0d	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 0 < e$
89		2re	$⊢ 2 \in ℝ$
90	60	adantllr	$⊢ (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to f (y) \in ℤ$
91	90	adantlr	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to f (y) \in ℤ$
92		2pos	$⊢ 0 < 2$
93	92	a1i	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 0 < 2$
94		expgt0	$⊢ (2 \in ℝ \land f (y) \in ℤ \land 0 < 2) \to 0 < 2^{f (y)}$
95	89 91 93 94	mp3an2i	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 0 < 2^{f (y)}$
96	83 86 88 95	divgt0d	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 0 < \frac{e}{2^{f (y)}}$
97	65 53	ltaddposd	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to (0 < \frac{e}{2^{f (y)}} \leftrightarrow M (A) < M (A) + (\frac{e}{2^{f (y)}}))$
98	96 97	mpbid	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to M (A) < M (A) + (\frac{e}{2^{f (y)}})$
99	81 98	eqbrtrrd	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <) < M (A) + (\frac{e}{2^{f (y)}})$
100		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
101		xrltso	$⊢ < Or ℝ^{*}$
102		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
103	100 101 102	mp2	$⊢ < Or [0, +∞]$
104	103	a1i	$⊢ (φ \land y \in X) \to < Or [0, +∞]$
105		omscl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \in 𝒫 ⋃ dom R) \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
106	76 77 48 105	syl3anc	$⊢ (φ \land y \in X) \to ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
107		xrge0infss	$⊢ ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \subseteq [0, +∞] \to \exists v \in [0, +∞] (\forall h \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg h < v \land \forall h \in [0, +∞] (v < h \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) u < h))$
108	106 107	syl	$⊢ (φ \land y \in X) \to \exists v \in [0, +∞] (\forall h \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg h < v \land \forall h \in [0, +∞] (v < h \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < h))$
109	104 108	infglb	$⊢ (φ \land y \in X) \to ((M (A) + (\frac{e}{2^{f (y)}}) \in [0, +∞] \land inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <) < M (A) + (\frac{e}{2^{f (y)}})) \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}}))$
110	109	imp	$⊢ ((φ \land y \in X) \land (M (A) + (\frac{e}{2^{f (y)}}) \in [0, +∞] \land inf (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <) < M (A) + (\frac{e}{2^{f (y)}}))) \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}})$
111	33 34 74 99 110	syl22anc	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}})$
112		eqid	$⊢ (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) = (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w))$
113		esumex	$⊢ \underset{w \in x}{\sum^{*}} R (w) \in V$
114	112 113	elrnmpti	$⊢ u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w)$
115	114	anbi1i	$⊢ (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
116		r19.41v	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
117	115 116	bitr4i	$⊢ (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
118	117	exbii	$⊢ \exists u (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow \exists u \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
119		df-rex	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \exists u (u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
120		rexcom4	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow \exists u \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
121	118 119 120	3bitr4i	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}}))$
122		breq1	$⊢ u = \underset{w \in x}{\sum^{}} R (w) \to (u < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
123	122	biimpa	$⊢ (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
124	123	exlimiv	$⊢ \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
125	124	reximi	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \exists u (u = \underset{w \in x}{\sum^{}} R (w) \land u < M (A) + (\frac{e}{2^{f (y)}})) \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
126	121 125	sylbi	$⊢ \exists u \in ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < M (A) + (\frac{e}{2^{f (y)}}) \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
127	111 126	syl	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
128		simpr	$⊢ (A \subseteq ⋃ z \land z ≼ ω) \to z ≼ ω$
129	128	a1i	$⊢ z \in 𝒫 dom R \to ((A \subseteq ⋃ z \land z ≼ ω) \to z ≼ ω)$
130	129	ss2rabi	$⊢ \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}$
131		rexss	$⊢ \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
132	130 131	ax-mp	$⊢ \exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
133		unieq	$⊢ z = x \to ⋃ z = ⋃ x$
134	133	sseq2d	$⊢ z = x \to (A \subseteq ⋃ z \leftrightarrow A \subseteq ⋃ x)$
135		breq1	$⊢ z = x \to (z ≼ ω \leftrightarrow x ≼ ω)$
136	134 135	anbi12d	$⊢ z = x \to ((A \subseteq ⋃ z \land z ≼ ω) \leftrightarrow (A \subseteq ⋃ x \land x ≼ ω))$
137	136	elrab	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \leftrightarrow (x \in 𝒫 dom R \land (A \subseteq ⋃ x \land x ≼ ω))$
138	137	simprbi	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to (A \subseteq ⋃ x \land x ≼ ω)$
139	138	simpld	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to A \subseteq ⋃ x$
140	139	a1i	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to A \subseteq ⋃ x)$
141	140	anim1d	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to ((x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
142	141	reximdv	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to (\exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
143	132 142	biimtrid	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to (\exists x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \to \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
144	127 143	mpd	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
145	32 144	ralrimia	$⊢ (((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \forall y \in X \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
146		unieq	$⊢ x = g (y) \to ⋃ x = ⋃ g (y)$
147	146	sseq2d	$⊢ x = g (y) \to (A \subseteq ⋃ x \leftrightarrow A \subseteq ⋃ g (y))$
148		esumeq1	$⊢ x = g (y) \to \underset{w \in x}{\sum^{}} R (w) = \underset{w \in g (y)}{\sum^{}} R (w)$
149	148	breq1d	$⊢ x = g (y) \to (\underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \leftrightarrow \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
150	147 149	anbi12d	$⊢ x = g (y) \to ((A \subseteq ⋃ x \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \leftrightarrow (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
151	150	ac6	$⊢ (X \in V \land \{z \in 𝒫 dom R \| z ≼ ω\} \in V \land \forall y \in X \exists x \in \{z \in 𝒫 dom R \| z ≼ ω\} (A \subseteq ⋃ x \land \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \exists g (g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
152	16 23 145 151	syl3anc	$⊢ (((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \exists g (g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
153		simp-5l	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to φ$
154	43	ralrimiva	$⊢ φ \to \forall y \in X A \in V$
155		iunexg	$⊢ (X \in V \land \forall y \in X A \in V) \to ⋃_{y \in X} A \in V$
156	15 154 155	syl2anc	$⊢ φ \to ⋃_{y \in X} A \in V$
157	47	iunssd	$⊢ φ \to ⋃_{y \in X} A \subseteq ⋃ dom R$
158	156 157	elpwd	$⊢ φ \to ⋃_{y \in X} A \in 𝒫 ⋃ dom R$
159	39 158	ffvelcdmd	$⊢ φ \to M (⋃_{y \in X} A) \in [0, +∞]$
160	100 159	sselid	$⊢ φ \to M (⋃_{y \in X} A) \in ℝ^{*}$
161	153 160	syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to M (⋃_{y \in X} A) \in ℝ^{*}$
162		simplr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
163	35	ad4antr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to X \in V$
164	162 163	fexd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to g \in V$
165		rnexg	$⊢ g \in V \to ran g \in V$
166		uniexg	$⊢ ran g \in V \to ⋃ ran g \in V$
167	164 165 166	3syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃ ran g \in V$
168	3	ad2antrr	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to R : Q ⟶ [0, +∞]$
169		frn	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}$
170		ssrab2	$⊢ \{z \in 𝒫 dom R \| z ≼ ω\} \subseteq 𝒫 dom R$
171	169 170	sstrdi	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq 𝒫 dom R$
172	171	unissd	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq ⋃ 𝒫 dom R$
173		unipw	$⊢ ⋃ 𝒫 dom R = dom R$
174	172 173	sseqtrdi	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq dom R$
175	174	adantl	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g \subseteq dom R$
176	44	adantr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to dom R = Q$
177	175 176	sseqtrd	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g \subseteq Q$
178	177	sselda	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to c \in Q$
179	168 178	ffvelcdmd	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to R (c) \in [0, +∞]$
180	179	ralrimiva	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \forall c \in ⋃ ran g R (c) \in [0, +∞]$
181	153 162 180	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \forall c \in ⋃ ran g R (c) \in [0, +∞]$
182		nfcv	$⊢ \underline{Ⅎ} c ⋃ ran g$
183	182	esumcl	$⊢ (⋃ ran g \in V \land \forall c \in ⋃ ran g R (c) \in [0, +∞]) \to \underset{c \in ⋃ ran g}{\sum^{*}} R (c) \in [0, +∞]$
184	167 181 183	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{c \in ⋃ ran g}{\sum^{*}} R (c) \in [0, +∞]$
185	100 184	sselid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ℝ^{}$
186		simp-5r	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{*}} M (A) \in ℝ$
187	186	rexrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} M (A) \in ℝ^{}$
188		simpllr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to e \in ℝ^{+}$
189	188	rpxrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to e \in ℝ^{*}$
190	187 189	xaddcld	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} M (A) +_{𝑒} e \in ℝ^{}$
191	169	ad2antlr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}$
192		sstr	$⊢ (ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \land \{z \in 𝒫 dom R \| z ≼ ω\} \subseteq 𝒫 dom R) \to ran g \subseteq 𝒫 dom R$
193	170 192	mpan2	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq 𝒫 dom R$
194		sspwuni	$⊢ ran g \subseteq 𝒫 dom R \leftrightarrow ⋃ ran g \subseteq dom R$
195	193 194	sylib	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq dom R$
196	191 195	syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃ ran g \subseteq dom R$
197		ffn	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to g Fn X$
198	197	ad2antlr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to g Fn X$
199	153 5	syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to X ≼ ω$
200		fnct	$⊢ (g Fn X \land X ≼ ω) \to g ≼ ω$
201		rnct	$⊢ g ≼ ω \to ran g ≼ ω$
202	200 201	syl	$⊢ (g Fn X \land X ≼ ω) \to ran g ≼ ω$
203		dfss3	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \leftrightarrow \forall w \in ran g w \in \{z \in 𝒫 dom R \| z ≼ ω\}$
204		breq1	$⊢ z = w \to (z ≼ ω \leftrightarrow w ≼ ω)$
205	204	elrab	$⊢ w \in \{z \in 𝒫 dom R \| z ≼ ω\} \leftrightarrow (w \in 𝒫 dom R \land w ≼ ω)$
206	205	simprbi	$⊢ w \in \{z \in 𝒫 dom R \| z ≼ ω\} \to w ≼ ω$
207	206	ralimi	$⊢ \forall w \in ran g w \in \{z \in 𝒫 dom R \| z ≼ ω\} \to \forall w \in ran g w ≼ ω$
208	203 207	sylbi	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to \forall w \in ran g w ≼ ω$
209		unictb	$⊢ (ran g ≼ ω \land \forall w \in ran g w ≼ ω) \to ⋃ ran g ≼ ω$
210	202 208 209	syl2an	$⊢ ((g Fn X \land X ≼ ω) \land ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g ≼ ω$
211	198 199 191 210	syl21anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃ ran g ≼ ω$
212		ctex	$⊢ ⋃ ran g ≼ ω \to ⋃ ran g \in V$
213		elpwg	$⊢ ⋃ ran g \in V \to (⋃ ran g \in 𝒫 dom R \leftrightarrow ⋃ ran g \subseteq dom R)$
214	211 212 213	3syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to (⋃ ran g \in 𝒫 dom R \leftrightarrow ⋃ ran g \subseteq dom R)$
215	196 214	mpbird	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃ ran g \in 𝒫 dom R$
216		simpl	$⊢ (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to A \subseteq ⋃ g (y)$
217	216	ralimi	$⊢ \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \forall y \in X A \subseteq ⋃ g (y)$
218		fvssunirn	$⊢ g (y) \subseteq ⋃ ran g$
219	218	unissi	$⊢ ⋃ g (y) \subseteq ⋃ ⋃ ran g$
220		sstr	$⊢ (A \subseteq ⋃ g (y) \land ⋃ g (y) \subseteq ⋃ ⋃ ran g) \to A \subseteq ⋃ ⋃ ran g$
221	219 220	mpan2	$⊢ A \subseteq ⋃ g (y) \to A \subseteq ⋃ ⋃ ran g$
222	221	ralimi	$⊢ \forall y \in X A \subseteq ⋃ g (y) \to \forall y \in X A \subseteq ⋃ ⋃ ran g$
223		iunss	$⊢ ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \leftrightarrow \forall y \in X A \subseteq ⋃ ⋃ ran g$
224	222 223	sylibr	$⊢ \forall y \in X A \subseteq ⋃ g (y) \to ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g$
225	217 224	syl	$⊢ \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g$
226	225	adantl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g$
227	215 226 211	jca32	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to (⋃ ran g \in 𝒫 dom R \land (⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \land ⋃ ran g ≼ ω))$
228		unieq	$⊢ z = ⋃ ran g \to ⋃ z = ⋃ ⋃ ran g$
229	228	sseq2d	$⊢ z = ⋃ ran g \to (⋃_{y \in X} A \subseteq ⋃ z \leftrightarrow ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g)$
230		breq1	$⊢ z = ⋃ ran g \to (z ≼ ω \leftrightarrow ⋃ ran g ≼ ω)$
231	229 230	anbi12d	$⊢ z = ⋃ ran g \to ((⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω) \leftrightarrow (⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \land ⋃ ran g ≼ ω))$
232	231	elrab	$⊢ ⋃ ran g \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \leftrightarrow (⋃ ran g \in 𝒫 dom R \land (⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \land ⋃ ran g ≼ ω))$
233	227 232	sylibr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to ⋃ ran g \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\}$
234		fveq2	$⊢ c = w \to R (c) = R (w)$
235	234	cbvesumv	$⊢ \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)$
236		esumeq1	$⊢ x = ⋃ ran g \to \underset{w \in x}{\sum^{}} R (w) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)$
237	236	rspceeqv	$⊢ (⋃ ran g \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \land \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)) \to \exists x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in x}{\sum^{}} R (w)$
238	233 235 237	sylancl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \exists x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in x}{\sum^{}} R (w)$
239		esumex	$⊢ \underset{c \in ⋃ ran g}{\sum^{*}} R (c) \in V$
240		eqid	$⊢ (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) = (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w))$
241	240	elrnmpt	$⊢ \underset{c \in ⋃ ran g}{\sum^{}} R (c) \in V \to (\underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in x}{\sum^{*}} R (w))$
242	239 241	ax-mp	$⊢ \underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in x}{\sum^{}} R (w)$
243	238 242	sylibr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w))$
244	103	a1i	$⊢ φ \to < Or [0, +∞]$
245		omscl	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land ⋃_{y \in X} A \in 𝒫 ⋃ dom R) \to ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
246	2 3 158 245	syl3anc	$⊢ φ \to ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) \subseteq [0, +∞]$
247		xrge0infss	$⊢ ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \subseteq [0, +∞] \to \exists e \in [0, +∞] (\forall t \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg t < e \land \forall t \in [0, +∞] (e < t \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) u < t))$
248	246 247	syl	$⊢ φ \to \exists e \in [0, +∞] (\forall t \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \neg t < e \land \forall t \in [0, +∞] (e < t \to \exists u \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) u < t))$
249	244 248	inflb	$⊢ φ \to (\underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \to \neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <))$
250	1	fveq1i	$⊢ M (⋃_{y \in X} A) = toOMeas (R) (⋃_{y \in X} A)$
251	4	iunssd	$⊢ φ \to ⋃_{y \in X} A \subseteq ⋃ Q$
252		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land ⋃_{y \in X} A \subseteq ⋃ Q) \to toOMeas (R) (⋃_{y \in X} A) = inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
253	2 3 251 252	syl3anc	$⊢ φ \to toOMeas (R) (⋃_{y \in X} A) = inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
254	250 253	eqtrid	$⊢ φ \to M (⋃_{y \in X} A) = inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
255	254	breq2d	$⊢ φ \to (\underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A) \leftrightarrow \underset{c \in ⋃ ran g}{\sum^{}} R (c) < inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <))$
256	255	notbid	$⊢ φ \to (\neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A) \leftrightarrow \neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < inf (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <))$
257	249 256	sylibrd	$⊢ φ \to (\underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) \to \neg \underset{c \in ⋃ ran g}{\sum^{*}} R (c) < M (⋃_{y \in X} A))$
258	153 243 257	sylc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \neg \underset{c \in ⋃ ran g}{\sum^{*}} R (c) < M (⋃_{y \in X} A)$
259	161 185 258	xrnltled	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to M (⋃_{y \in X} A) \leq \underset{c \in ⋃ ran g}{\sum^{*}} R (c)$
260		nfv	$⊢ Ⅎ y g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
261	32 260	nfan	$⊢ Ⅎ y ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\})$
262		nfra1	$⊢ Ⅎ y \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
263	261 262	nfan	$⊢ Ⅎ y (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))$
264		simp-6l	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to φ$
265		simpllr	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
266		simpr	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to y \in X$
267		fvex	$⊢ g (y) \in V$
268	3	ad3antrrr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to R : Q ⟶ [0, +∞]$
269		simpllr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
270		simplr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to y \in X$
271	269 270	ffvelcdmd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \in \{z \in 𝒫 dom R \| z ≼ ω\}$
272	170 271	sselid	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \in 𝒫 dom R$
273	272	elpwid	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \subseteq dom R$
274	268 273	fssdmd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \subseteq Q$
275		simpr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to w \in g (y)$
276	274 275	sseldd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to w \in Q$
277	268 276	ffvelcdmd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to R (w) \in [0, +∞]$
278	277	ralrimiva	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \forall w \in g (y) R (w) \in [0, +∞]$
279		nfcv	$⊢ \underline{Ⅎ} w g (y)$
280	279	esumcl	$⊢ (g (y) \in V \land \forall w \in g (y) R (w) \in [0, +∞]) \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
281	267 278 280	sylancr	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
282	264 265 266 281	syl21anc	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
283	263 282	ralrimia	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \forall y \in X \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
284	25	esumcl	$⊢ (X \in V \land \forall y \in X \underset{w \in g (y)}{\sum^{}} R (w) \in [0, +∞]) \to \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
285	163 283 284	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w) \in [0, +∞]$
286	100 285	sselid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w) \in ℝ^{*}$
287		nfv	$⊢ Ⅎ w (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\})$
288		simpr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
289		fniunfv	$⊢ g Fn X \to ⋃_{y \in X} g (y) = ⋃ ran g$
290	288 197 289	3syl	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃_{y \in X} g (y) = ⋃ ran g$
291	287 290	esumeq1d	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \underset{w \in ⋃_{y \in X} g (y)}{\sum^{}} R (w) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)$
292	15	adantr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to X \in V$
293	267	a1i	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to g (y) \in V$
294	292 293 277	esumiun	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \underset{w \in ⋃_{y \in X} g (y)}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{*}} R (w)$
295	291 294	eqbrtrrd	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \underset{w \in ⋃ ran g}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{*}} R (w)$
296	295	ad5ant15	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \underset{w \in ⋃ ran g}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w)$
297	296	adantr	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{w \in ⋃ ran g}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{*}} R (w)$
298	235 297	eqbrtrid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{c \in ⋃ ran g}{\sum^{}} R (c) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{*}} R (w)$
299	264 266 49	syl2anc	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to M (A) \in [0, +∞]$
300	72	ad4ant14	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to \frac{e}{2^{f (y)}} \in [0, +∞]$
301	299 300	xrge0addcld	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in [0, +∞]$
302	263 301	ralrimia	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \forall y \in X M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in [0, +∞]$
303	25	esumcl	$⊢ (X \in V \land \forall y \in X M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in [0, +∞]) \to \underset{y \in X}{\sum^{*}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) \in [0, +∞]$
304	163 302 303	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{*}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) \in [0, +∞]$
305	100 304	sselid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) \in ℝ^{}$
306	199 14	syl	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to X \in V$
307	52	ad5ant15	$⊢ (((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to M (A) \in ℝ$
308	307	adantr	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to M (A) \in ℝ$
309	65	adantlr	$⊢ (((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ$
310	309	adantr	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \frac{e}{2^{f (y)}} \in ℝ$
311		simpr	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}})$
312		rexadd	$⊢ (M (A) \in ℝ \land \frac{e}{2^{f (y)}} \in ℝ) \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) = M (A) + (\frac{e}{2^{f (y)}})$
313	312	breq2d	$⊢ (M (A) \in ℝ \land \frac{e}{2^{f (y)}} \in ℝ) \to (\underset{w \in g (y)}{\sum^{}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \leftrightarrow \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
314	313	biimpar	$⊢ ((M (A) \in ℝ \land \frac{e}{2^{f (y)}} \in ℝ) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in g (y)}{\sum^{}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}})$
315	308 310 311 314	syl21anc	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}})$
316	315	ex	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to (\underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \to \underset{w \in g (y)}{\sum^{*}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
317		simp-5l	$⊢ (((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to φ$
318		simplr	$⊢ (((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
319		simpr	$⊢ (((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to y \in X$
320	317 318 319 281	syl21anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \underset{w \in g (y)}{\sum^{}} R (w) \in [0, +∞]$
321	100 320	sselid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \underset{w \in g (y)}{\sum^{}} R (w) \in ℝ^{*}$
322	307	rexrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to M (A) \in ℝ^{}$
323	309	rexrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ^{}$
324	322 323	xaddcld	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in ℝ^{}$
325		xrltle	$⊢ (\underset{w \in g (y)}{\sum^{}} R (w) \in ℝ^{} \land M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in ℝ^{}) \to (\underset{w \in g (y)}{\sum^{}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \to \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
326	321 324 325	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to (\underset{w \in g (y)}{\sum^{}} R (w) < M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \to \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
327	316 326	syld	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to (\underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \to \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
328	327	adantld	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to ((A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
329	261 328	ralimdaa	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to (\forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})) \to \forall y \in X \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
330	329	imp	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \forall y \in X \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}})$
331	330	r19.21bi	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}})$
332	263 25 306 282 301 331	esumlef	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{*}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
333	153 49	sylan	$⊢ ((((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \land y \in X) \to M (A) \in [0, +∞]$
334	263 25 306 333 300	esumaddf	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) = \underset{y \in X}{\sum^{}} M (A) +_{𝑒} \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}})$
335	263 300	ralrimia	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \forall y \in X \frac{e}{2^{f (y)}} \in [0, +∞]$
336	25	esumcl	$⊢ (X \in V \land \forall y \in X \frac{e}{2^{f (y)}} \in [0, +∞]) \to \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}}) \in [0, +∞]$
337	163 335 336	syl2anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}}) \in [0, +∞]$
338	100 337	sselid	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) \in ℝ^{}$
339		simp-4r	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to f : X \underset{1-1}{⟶} ℕ$
340		vex	$⊢ f \in V$
341	340	rnex	$⊢ ran f \in V$
342	58	frnd	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ran f \subseteq ℕ$
343	342	adantr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to ran f \subseteq ℕ$
344	343	sselda	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ran f) \to z \in ℕ$
345	55	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to 2 \in ℝ^{+}$
346		simpr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to z \in ℕ$
347	346	nnzd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to z \in ℤ$
348	345 347	rpexpcld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to 2^{z} \in ℝ^{+}$
349	348	rpreccld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in ℝ^{+}$
350	70 349	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞]$
351	350	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞]$
352	344 351	syldan	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ran f) \to \frac{1}{2^{z}} \in [0, +∞]$
353	352	ralrimiva	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \forall z \in ran f \frac{1}{2^{z}} \in [0, +∞]$
354		nfcv	$⊢ \underline{Ⅎ} z ran f$
355	354	esumcl	$⊢ (ran f \in V \land \forall z \in ran f \frac{1}{2^{z}} \in [0, +∞]) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \in [0, +∞]$
356	341 353 355	sylancr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \in [0, +∞]$
357	100 356	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \in ℝ^{}$
358		1xr	$⊢ 1 \in ℝ^{*}$
359	358	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to 1 \in ℝ^{*}$
360	70	sseli	$⊢ e \in ℝ^{+} \to e \in [0, +∞]$
361	360	adantl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in [0, +∞]$
362		elxrge0	$⊢ e \in [0, +∞] \leftrightarrow (e \in ℝ^{*} \land 0 \leq e)$
363	361 362	sylib	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to (e \in ℝ^{*} \land 0 \leq e)$
364		nfv	$⊢ Ⅎ z (φ \land f : X \underset{1-1}{⟶} ℕ)$
365		nnex	$⊢ ℕ \in V$
366	365	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ℕ \in V$
367	364 366 350 342	esummono	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \leq \underset{z \in ℕ}{\sum^{}} (\frac{1}{2^{z}})$
368		oveq2	$⊢ z = w \to 2^{z} = 2^{w}$
369	368	oveq2d	$⊢ z = w \to \frac{1}{2^{z}} = \frac{1}{2^{w}}$
370		ioossico	$⊢ (0, +∞) \subseteq [0, +∞)$
371	68 370	eqsstri	$⊢ ℝ^{+} \subseteq [0, +∞)$
372	371 349	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞)$
373		eqidd	$⊢ z \in ℕ \to (w \in ℕ ⟼ \frac{1}{2^{w}}) = (w \in ℕ ⟼ \frac{1}{2^{w}})$
374		simpr	$⊢ (z \in ℕ \land w = z) \to w = z$
375	374	oveq2d	$⊢ (z \in ℕ \land w = z) \to 2^{w} = 2^{z}$
376	375	oveq2d	$⊢ (z \in ℕ \land w = z) \to \frac{1}{2^{w}} = \frac{1}{2^{z}}$
377		id	$⊢ z \in ℕ \to z \in ℕ$
378		ovexd	$⊢ z \in ℕ \to \frac{1}{2^{z}} \in V$
379	373 376 377 378	fvmptd	$⊢ z \in ℕ \to (w \in ℕ ⟼ \frac{1}{2^{w}}) (z) = \frac{1}{2^{z}}$
380	379	adantl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to (w \in ℕ ⟼ \frac{1}{2^{w}}) (z) = \frac{1}{2^{z}}$
381		ax-1cn	$⊢ 1 \in ℂ$
382		eqid	$⊢ (w \in ℕ ⟼ \frac{1}{2^{w}}) = (w \in ℕ ⟼ \frac{1}{2^{w}})$
383	382	geo2lim	$⊢ 1 \in ℂ \to seq 1 (+ (w \in ℕ ⟼ \frac{1}{2^{w}})) ⇝ 1$
384	381 383	mp1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to seq 1 (+ (w \in ℕ ⟼ \frac{1}{2^{w}})) ⇝ 1$
385		1red	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to 1 \in ℝ$
386	369 372 380 384 385	esumcvgsum	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ℕ}{\sum^{*}} (\frac{1}{2^{z}}) = \sum_{z \in ℕ} (\frac{1}{2^{z}})$
387		geoihalfsum	$⊢ \sum_{z \in ℕ} (\frac{1}{2^{z}}) = 1$
388	386 387	eqtrdi	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ℕ}{\sum^{*}} (\frac{1}{2^{z}}) = 1$
389	367 388	breqtrd	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \leq 1$
390	389	adantr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \leq 1$
391		xlemul2a	$⊢ ((\underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \in ℝ^{} \land 1 \in ℝ^{} \land (e \in ℝ^{} \land 0 \leq e)) \land \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \leq 1) \to e \cdot_{𝑒} \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \leq e \cdot_{𝑒} 1$
392	357 359 363 390 391	syl31anc	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \leq e \cdot_{𝑒} 1$
393	54	rpcnd	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℂ$
394	61	rpcnd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \in ℂ$
395	394	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℂ$
396		2cnd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \in ℂ$
397		2ne0	$⊢ 2 \neq 0$
398	397	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \neq 0$
399	396 398 60	expne0d	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \neq 0$
400	399	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \neq 0$
401	393 395 400	divrecd	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} = e (\frac{1}{2^{f (y)}})$
402	61	rpreccld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ^{+}$
403	402	rpred	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ$
404	403	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ$
405		rexmul	$⊢ (e \in ℝ \land \frac{1}{2^{f (y)}} \in ℝ) \to e \cdot_{𝑒} (\frac{1}{2^{f (y)}}) = e (\frac{1}{2^{f (y)}})$
406	82 404 405	syl2anc	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \cdot_{𝑒} (\frac{1}{2^{f (y)}}) = e (\frac{1}{2^{f (y)}})$
407	401 406	eqtr4d	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} = e \cdot_{𝑒} (\frac{1}{2^{f (y)}})$
408	407	esumeq2dv	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) = \underset{y \in X}{\sum^{}} (e \cdot_{𝑒} (\frac{1}{2^{f (y)}}))$
409	15	ad2antrr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to X \in V$
410	70 402	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in [0, +∞]$
411	410	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{1}{2^{f (y)}} \in [0, +∞]$
412	371	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ℝ^{+} \subseteq [0, +∞)$
413	412	sselda	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in [0, +∞)$
414	409 411 413	esummulc2	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} \underset{y \in X}{\sum^{}} (\frac{1}{2^{f (y)}}) = \underset{y \in X}{\sum^{}} (e \cdot_{𝑒} (\frac{1}{2^{f (y)}}))$
415		nfcv	$⊢ \underline{Ⅎ} y (\frac{1}{2^{z}})$
416		nfv	$⊢ Ⅎ y (φ \land f : X \underset{1-1}{⟶} ℕ)$
417		oveq2	$⊢ z = f (y) \to 2^{z} = 2^{f (y)}$
418	417	oveq2d	$⊢ z = f (y) \to \frac{1}{2^{z}} = \frac{1}{2^{f (y)}}$
419	15	adantr	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to X \in V$
420		df-f1	$⊢ f : X \underset{1-1}{⟶} ℕ \leftrightarrow (f : X ⟶ ℕ \land Fun f^{-1})$
421	420	simprbi	$⊢ f : X \underset{1-1}{⟶} ℕ \to Fun f^{-1}$
422	57	feqmptd	$⊢ f : X \underset{1-1}{⟶} ℕ \to f = (y \in X ⟼ f (y))$
423	422	cnveqd	$⊢ f : X \underset{1-1}{⟶} ℕ \to f^{-1} = {(y \in X ⟼ f (y))}^{-1}$
424	423	funeqd	$⊢ f : X \underset{1-1}{⟶} ℕ \to (Fun f^{-1} \leftrightarrow Fun {(y \in X ⟼ f (y))}^{-1})$
425	421 424	mpbid	$⊢ f : X \underset{1-1}{⟶} ℕ \to Fun {(y \in X ⟼ f (y))}^{-1}$
426	425	adantl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to Fun {(y \in X ⟼ f (y))}^{-1}$
427	415 416 25 418 419 426 410 59	esumc	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{y \in X}{\sum^{}} (\frac{1}{2^{f (y)}}) = \underset{z \in \{x \| \exists y \in X x = f (y)\}}{\sum^{}} (\frac{1}{2^{z}})$
428		ffn	$⊢ f : X ⟶ ℕ \to f Fn X$
429		fnrnfv	$⊢ f Fn X \to ran f = \{x \| \exists y \in X x = f (y)\}$
430	58 428 429	3syl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ran f = \{x \| \exists y \in X x = f (y)\}$
431	364 430	esumeq1d	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) = \underset{z \in \{x \| \exists y \in X x = f (y)\}}{\sum^{}} (\frac{1}{2^{z}})$
432	427 431	eqtr4d	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{y \in X}{\sum^{}} (\frac{1}{2^{f (y)}}) = \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}})$
433	432	adantr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{y \in X}{\sum^{}} (\frac{1}{2^{f (y)}}) = \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}})$
434	433	oveq2d	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} \underset{y \in X}{\sum^{}} (\frac{1}{2^{f (y)}}) = e \cdot_{𝑒} \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}})$
435	408 414 434	3eqtr2rd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) = \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}})$
436	363	simpld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in ℝ^{*}$
437		xmulrid	$⊢ e \in ℝ^{*} \to e \cdot_{𝑒} 1 = e$
438	436 437	syl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} 1 = e$
439	392 435 438	3brtr3d	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}}) \leq e$
440	153 339 188 439	syl21anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}}) \leq e$
441		xleadd2a	$⊢ ((\underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) \in ℝ^{} \land e \in ℝ^{} \land \underset{y \in X}{\sum^{}} M (A) \in ℝ^{}) \land \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) \leq e) \to \underset{y \in X}{\sum^{}} M (A) +_{𝑒} \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) \leq \underset{y \in X}{\sum^{*}} M (A) +_{𝑒} e$
442	338 189 187 440 441	syl31anc	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} M (A) +_{𝑒} \underset{y \in X}{\sum^{}} (\frac{e}{2^{f (y)}}) \leq \underset{y \in X}{\sum^{*}} M (A) +_{𝑒} e$
443	334 442	eqbrtrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} (M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) \leq \underset{y \in X}{\sum^{}} M (A) +_{𝑒} e$
444	286 305 190 332 443	xrletrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{*}} M (A) +_{𝑒} e$
445	185 286 190 298 444	xrletrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{c \in ⋃ ran g}{\sum^{}} R (c) \leq \underset{y \in X}{\sum^{}} M (A) +_{𝑒} e$
446	161 185 190 259 445	xrletrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) +_{𝑒} e$
447	188	rpred	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to e \in ℝ$
448	186 447	rexaddd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to \underset{y \in X}{\sum^{}} M (A) +_{𝑒} e = \underset{y \in X}{\sum^{}} M (A) + e$
449	446 448	breqtrd	$⊢ (((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) + e$
450	449	anasss	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land (g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \land \forall y \in X (A \subseteq ⋃ g (y) \land \underset{w \in g (y)}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}})))) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) + e$
451	152 450	exlimddv	$⊢ (((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) + e$
452	451	ralrimiva	$⊢ ((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \to \forall e \in ℝ^{+} M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) + e$
453		xralrple	$⊢ (M (⋃_{y \in X} A) \in ℝ^{} \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to (M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) \leftrightarrow \forall e \in ℝ^{+} M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) + e)$
454	160 453	sylan	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to (M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) \leftrightarrow \forall e \in ℝ^{+} M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) + e)$
455	454	adantr	$⊢ ((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \to (M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A) \leftrightarrow \forall e \in ℝ^{+} M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) + e)$
456	452 455	mpbird	$⊢ ((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A)$
457	12 456	exlimddv	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A)$
458	160	adantr	$⊢ (φ \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \in ℝ^{}$
459	458	pnfged	$⊢ (φ \land \neg \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \leq +∞$
460	49	ralrimiva	$⊢ φ \to \forall y \in X M (A) \in [0, +∞]$
461	25	esumcl	$⊢ (X \in V \land \forall y \in X M (A) \in [0, +∞]) \to \underset{y \in X}{\sum^{*}} M (A) \in [0, +∞]$
462	15 460 461	syl2anc	$⊢ φ \to \underset{y \in X}{\sum^{*}} M (A) \in [0, +∞]$
463		xrge0nre	$⊢ (\underset{y \in X}{\sum^{}} M (A) \in [0, +∞] \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to \underset{y \in X}{\sum^{*}} M (A) = +∞$
464	462 463	sylan	$⊢ (φ \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to \underset{y \in X}{\sum^{}} M (A) = +∞$
465	459 464	breqtrrd	$⊢ (φ \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A)$
466	457 465	pm2.61dan	$⊢ φ \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A)$

Metamath Proof Explorer

Theorem omssubadd

Proof