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)

	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	6	ensymi	$⊢ ω \approx ℕ$
8		domentr	$⊢ (X ≼ ω \land ω \approx ℕ) \to X ≼ ℕ$
9	5 7 8	sylancl	$⊢ φ \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		nfv	$⊢ Ⅎ y φ$
18		nfcv	$⊢ \underline{Ⅎ} y X$
19	18	nfesum1	$⊢ \underline{Ⅎ} y \underset{y \in X}{\sum^{*}} M (A)$
20		nfcv	$⊢ \underline{Ⅎ} y ℝ$
21	19 20	nfel	$⊢ Ⅎ y \underset{y \in X}{\sum^{*}} M (A) \in ℝ$
22	17 21	nfan	$⊢ Ⅎ y (φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ)$
23		nfv	$⊢ Ⅎ y f : X \underset{1-1}{⟶} ℕ$
24	22 23	nfan	$⊢ Ⅎ y ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ)$
25		nfv	$⊢ Ⅎ y e \in ℝ^{+}$
26	24 25	nfan	$⊢ Ⅎ y (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+})$
27	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 φ$
28		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$
29	15	adantr	$⊢ (φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \to X \in V$
30		omsf	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
31	1	feq1i	$⊢ M : 𝒫 ⋃ dom R ⟶ [0, +∞] \leftrightarrow toOMeas (R) : 𝒫 ⋃ dom R ⟶ [0, +∞]$
32	30 31	sylibr	$⊢ (Q \in V \land R : Q ⟶ [0, +∞]) \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
33	2 3 32	syl2anc	$⊢ φ \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
34	33	adantr	$⊢ (φ \land y \in X) \to M : 𝒫 ⋃ dom R ⟶ [0, +∞]$
35	3	fdmd	$⊢ φ \to dom R = Q$
36	35	unieqd	$⊢ φ \to ⋃ dom R = ⋃ Q$
37	36	adantr	$⊢ (φ \land y \in X) \to ⋃ dom R = ⋃ Q$
38	4 37	sseqtrrd	$⊢ (φ \land y \in X) \to A \subseteq ⋃ dom R$
39	2	uniexd	$⊢ φ \to ⋃ Q \in V$
40	39	adantr	$⊢ (φ \land y \in X) \to ⋃ Q \in V$
41		ssexg	$⊢ (A \subseteq ⋃ Q \land ⋃ Q \in V) \to A \in V$
42	4 40 41	syl2anc	$⊢ (φ \land y \in X) \to A \in V$
43		elpwg	$⊢ A \in V \to (A \in 𝒫 ⋃ dom R \leftrightarrow A \subseteq ⋃ dom R)$
44	42 43	syl	$⊢ (φ \land y \in X) \to (A \in 𝒫 ⋃ dom R \leftrightarrow A \subseteq ⋃ dom R)$
45	38 44	mpbird	$⊢ (φ \land y \in X) \to A \in 𝒫 ⋃ dom R$
46	34 45	ffvelrnd	$⊢ (φ \land y \in X) \to M (A) \in [0, +∞]$
47	46	adantlr	$⊢ ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land y \in X) \to M (A) \in [0, +∞]$
48		simpr	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to \underset{y \in X}{\sum^{}} M (A) \in ℝ$
49	22 29 47 48	esumcvgre	$⊢ ((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land y \in X) \to M (A) \in ℝ$
50	49	adantlr	$⊢ (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to M (A) \in ℝ$
51	50	adantlr	$⊢ ((((φ \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 ℝ$
52		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
53		simplr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ^{+}$
54		2rp	$⊢ 2 \in ℝ^{+}$
55	54	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \in ℝ^{+}$
56		df-f1	$⊢ f : X \underset{1-1}{⟶} ℕ \leftrightarrow (f : X ⟶ ℕ \land Fun f^{-1})$
57	56	simplbi	$⊢ f : X \underset{1-1}{⟶} ℕ \to f : X ⟶ ℕ$
58	57	adantl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to f : X ⟶ ℕ$
59	58	ffvelrnda	$⊢ ((φ \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	55 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	53 62	rpdivcld	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in ℝ^{+}$
64	52 63	sselid	$⊢ (((φ \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		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)}})$
67	51 65 66	syl2anc	$⊢ ((((φ \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)}})$
68	13 46	sylan	$⊢ ((((φ \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, +∞]$
69		dfrp2	$⊢ ℝ^{+} = (0, +∞)$
70		ioossicc	$⊢ (0, +∞) \subseteq [0, +∞]$
71	69 70	eqsstri	$⊢ ℝ^{+} \subseteq [0, +∞]$
72	71 63	sselid	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{e}{2^{f (y)}} \in [0, +∞]$
73	72	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, +∞]$
74	68 73	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, +∞]$
75	67 74	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, +∞]$
76	52 53	sselid	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℝ$
77	76	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 ℝ$
78	52 61	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \in ℝ$
79	78	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℝ$
80	79	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 ℝ$
81		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 ℝ^{+}$
82	81	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$
83		2re	$⊢ 2 \in ℝ$
84	83	a1i	$⊢ ((((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2 \in ℝ$
85	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 ℤ$
86	85	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 ℤ$
87		2pos	$⊢ 0 < 2$
88	87	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$
89		expgt0	$⊢ (2 \in ℝ \land f (y) \in ℤ \land 0 < 2) \to 0 < 2^{f (y)}$
90	84 86 88 89	syl3anc	$⊢ ((((φ \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)}$
91	77 80 82 90	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)}}$
92	65 51	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)}}))$
93	91 92	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)}})$
94	1	fveq1i	$⊢ M (A) = toOMeas (R) (A)$
95	2	adantr	$⊢ (φ \land y \in X) \to Q \in V$
96	3	adantr	$⊢ (φ \land y \in X) \to R : Q ⟶ [0, +∞]$
97		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land A \subseteq ⋃ Q) \to toOMeas (R) (A) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
98	95 96 4 97	syl3anc	$⊢ (φ \land y \in X) \to toOMeas (R) (A) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
99	94 98	syl5eq	$⊢ (φ \land y \in X) \to M (A) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
100	13 99	sylan	$⊢ ((((φ \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) = sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <)$
101	100	eqcomd	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to sup (ran (x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <) = M (A)$
102	101	breq1d	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to (sup (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)}}) \leftrightarrow M (A) < M (A) + (\frac{e}{2^{f (y)}}))$
103	93 102	mpbird	$⊢ ((((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to sup (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)}})$
104	75 103	jca	$⊢ ((((φ \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, +∞] \land sup (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)}}))$
105		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
106		xrltso	$⊢ < Or ℝ^{*}$
107		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
108	105 106 107	mp2	$⊢ < Or [0, +∞]$
109		biid	$⊢ < Or [0, +∞] \leftrightarrow < Or [0, +∞]$
110	108 109	mpbi	$⊢ < Or [0, +∞]$
111	110	a1i	$⊢ (φ \land y \in X) \to < Or [0, +∞]$
112		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, +∞]$
113	95 96 45 112	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, +∞]$
114		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))$
115	113 114	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))$
116	111 115	infglb	$⊢ (φ \land y \in X) \to ((M (A) + (\frac{e}{2^{f (y)}}) \in [0, +∞] \land sup (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)}}))$
117	116	imp	$⊢ ((φ \land y \in X) \land (M (A) + (\frac{e}{2^{f (y)}}) \in [0, +∞] \land sup (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)}})$
118	27 28 104 117	syl21anc	$⊢ ((((φ \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)}})$
119		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))$
120		esumex	$⊢ \underset{w \in x}{\sum^{*}} R (w) \in V$
121	119 120	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)$
122	121	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)}}))$
123		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)}}))$
124	122 123	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)}}))$
125	124	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)}}))$
126		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)}}))$
127		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)}}))$
128	125 126 127	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)}}))$
129		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)}}))$
130		idd	$⊢ u = \underset{w \in x}{\sum^{}} R (w) \to (\underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}) \to \underset{w \in x}{\sum^{*}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
131	129 130	sylbid	$⊢ u = \underset{w \in x}{\sum^{}} R (w) \to (u < M (A) + (\frac{e}{2^{f (y)}}) \to \underset{w \in x}{\sum^{}} R (w) < M (A) + (\frac{e}{2^{f (y)}}))$
132	131	imp	$⊢ (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)}})$
133	132	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)}})$
134	133	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)}})$
135	128 134	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)}})$
136	118 135	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)}})$
137		simpr	$⊢ (A \subseteq ⋃ z \land z ≼ ω) \to z ≼ ω$
138	137	a1i	$⊢ z \in 𝒫 dom R \to ((A \subseteq ⋃ z \land z ≼ ω) \to z ≼ ω)$
139	138	ss2rabi	$⊢ \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}$
140		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)}})))$
141	139 140	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)}}))$
142		unieq	$⊢ z = x \to ⋃ z = ⋃ x$
143	142	sseq2d	$⊢ z = x \to (A \subseteq ⋃ z \leftrightarrow A \subseteq ⋃ x)$
144		breq1	$⊢ z = x \to (z ≼ ω \leftrightarrow x ≼ ω)$
145	143 144	anbi12d	$⊢ z = x \to ((A \subseteq ⋃ z \land z ≼ ω) \leftrightarrow (A \subseteq ⋃ x \land x ≼ ω))$
146	145	elrab	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \leftrightarrow (x \in 𝒫 dom R \land (A \subseteq ⋃ x \land x ≼ ω))$
147	146	simprbi	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to (A \subseteq ⋃ x \land x ≼ ω)$
148	147	simpld	$⊢ x \in \{z \in 𝒫 dom R \| (A \subseteq ⋃ z \land z ≼ ω)\} \to A \subseteq ⋃ x$
149	148	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)$
150	149	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)}})))$
151	150	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)}})))$
152	141 151	syl5bi	$⊢ ((((φ \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)}})))$
153	136 152	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)}}))$
154	153	ex	$⊢ (((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to (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)}})))$
155	26 154	ralrimi	$⊢ (((φ \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)}}))$
156		unieq	$⊢ x = g (y) \to ⋃ x = ⋃ g (y)$
157	156	sseq2d	$⊢ x = g (y) \to (A \subseteq ⋃ x \leftrightarrow A \subseteq ⋃ g (y))$
158		esumeq1	$⊢ x = g (y) \to \underset{w \in x}{\sum^{}} R (w) = \underset{w \in g (y)}{\sum^{}} R (w)$
159	158	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)}}))$
160	157 159	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)}})))$
161	160	ac6sg	$⊢ X \in V \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)}})) \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)}}))))$
162	161	imp	$⊢ (X \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)}})))$
163	16 155 162	syl2anc	$⊢ (((φ \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)}})))$
164	13	ad2antrr	$⊢ (((((φ \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 φ$
165	38	ralrimiva	$⊢ φ \to \forall y \in X A \subseteq ⋃ dom R$
166		iunss	$⊢ ⋃_{y \in X} A \subseteq ⋃ dom R \leftrightarrow \forall y \in X A \subseteq ⋃ dom R$
167	165 166	sylibr	$⊢ φ \to ⋃_{y \in X} A \subseteq ⋃ dom R$
168	42	ralrimiva	$⊢ φ \to \forall y \in X A \in V$
169		iunexg	$⊢ (X \in V \land \forall y \in X A \in V) \to ⋃_{y \in X} A \in V$
170	15 168 169	syl2anc	$⊢ φ \to ⋃_{y \in X} A \in V$
171		elpwg	$⊢ ⋃_{y \in X} A \in V \to (⋃_{y \in X} A \in 𝒫 ⋃ dom R \leftrightarrow ⋃_{y \in X} A \subseteq ⋃ dom R)$
172	170 171	syl	$⊢ φ \to (⋃_{y \in X} A \in 𝒫 ⋃ dom R \leftrightarrow ⋃_{y \in X} A \subseteq ⋃ dom R)$
173	167 172	mpbird	$⊢ φ \to ⋃_{y \in X} A \in 𝒫 ⋃ dom R$
174	33 173	ffvelrnd	$⊢ φ \to M (⋃_{y \in X} A) \in [0, +∞]$
175	105 174	sselid	$⊢ φ \to M (⋃_{y \in X} A) \in ℝ^{*}$
176	164 175	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 ℝ^{*}$
177		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 ≼ ω\}$
178	29	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$
179	177 178	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$
180		rnexg	$⊢ g \in V \to ran g \in V$
181		uniexg	$⊢ ran g \in V \to ⋃ ran g \in V$
182	179 180 181	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$
183		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 φ$
184	3	ad2antrr	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to R : Q ⟶ [0, +∞]$
185		frn	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}$
186		ssrab2	$⊢ \{z \in 𝒫 dom R \| z ≼ ω\} \subseteq 𝒫 dom R$
187	185 186	sstrdi	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq 𝒫 dom R$
188	187	unissd	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq ⋃ 𝒫 dom R$
189		unipw	$⊢ ⋃ 𝒫 dom R = dom R$
190	188 189	sseqtrdi	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq dom R$
191	190	adantl	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g \subseteq dom R$
192	35	adantr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to dom R = Q$
193	191 192	sseqtrd	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g \subseteq Q$
194	193	sselda	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to c \in Q$
195	184 194	ffvelrnd	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land c \in ⋃ ran g) \to R (c) \in [0, +∞]$
196	195	ralrimiva	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to \forall c \in ⋃ ran g R (c) \in [0, +∞]$
197	183 177 196	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, +∞]$
198		nfcv	$⊢ \underline{Ⅎ} c ⋃ ran g$
199	198	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, +∞]$
200	182 197 199	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, +∞]$
201	105 200	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 ℝ^{}$
202		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 ℝ$
203	202	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 ℝ^{}$
204		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 ℝ^{+}$
205	204	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 ℝ^{*}$
206	203 205	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 ℝ^{}$
207	185	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 ≼ ω\}$
208		sstr	$⊢ (ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \land \{z \in 𝒫 dom R \| z ≼ ω\} \subseteq 𝒫 dom R) \to ran g \subseteq 𝒫 dom R$
209	186 208	mpan2	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to ran g \subseteq 𝒫 dom R$
210		sspwuni	$⊢ ran g \subseteq 𝒫 dom R \leftrightarrow ⋃ ran g \subseteq dom R$
211	209 210	sylib	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to ⋃ ran g \subseteq dom R$
212	207 211	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$
213		ffn	$⊢ g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\} \to g Fn X$
214	213	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$
215	164 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 ≼ ω$
216		fnct	$⊢ (g Fn X \land X ≼ ω) \to g ≼ ω$
217		rnct	$⊢ g ≼ ω \to ran g ≼ ω$
218	216 217	syl	$⊢ (g Fn X \land X ≼ ω) \to ran g ≼ ω$
219		dfss3	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \leftrightarrow \forall w \in ran g w \in \{z \in 𝒫 dom R \| z ≼ ω\}$
220	219	biimpi	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to \forall w \in ran g w \in \{z \in 𝒫 dom R \| z ≼ ω\}$
221		breq1	$⊢ z = w \to (z ≼ ω \leftrightarrow w ≼ ω)$
222	221	elrab	$⊢ w \in \{z \in 𝒫 dom R \| z ≼ ω\} \leftrightarrow (w \in 𝒫 dom R \land w ≼ ω)$
223	222	simprbi	$⊢ w \in \{z \in 𝒫 dom R \| z ≼ ω\} \to w ≼ ω$
224	223	ralimi	$⊢ \forall w \in ran g w \in \{z \in 𝒫 dom R \| z ≼ ω\} \to \forall w \in ran g w ≼ ω$
225	220 224	syl	$⊢ ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\} \to \forall w \in ran g w ≼ ω$
226		unictb	$⊢ (ran g ≼ ω \land \forall w \in ran g w ≼ ω) \to ⋃ ran g ≼ ω$
227	218 225 226	syl2an	$⊢ ((g Fn X \land X ≼ ω) \land ran g \subseteq \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃ ran g ≼ ω$
228	214 215 207 227	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 ≼ ω$
229		ctex	$⊢ ⋃ ran g ≼ ω \to ⋃ ran g \in V$
230		elpwg	$⊢ ⋃ ran g \in V \to (⋃ ran g \in 𝒫 dom R \leftrightarrow ⋃ ran g \subseteq dom R)$
231	228 229 230	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)$
232	212 231	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$
233		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)$
234	233	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)$
235		fvssunirn	$⊢ g (y) \subseteq ⋃ ran g$
236	235	unissi	$⊢ ⋃ g (y) \subseteq ⋃ ⋃ ran g$
237		sstr	$⊢ (A \subseteq ⋃ g (y) \land ⋃ g (y) \subseteq ⋃ ⋃ ran g) \to A \subseteq ⋃ ⋃ ran g$
238	236 237	mpan2	$⊢ A \subseteq ⋃ g (y) \to A \subseteq ⋃ ⋃ ran g$
239	238	ralimi	$⊢ \forall y \in X A \subseteq ⋃ g (y) \to \forall y \in X A \subseteq ⋃ ⋃ ran g$
240		iunss	$⊢ ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \leftrightarrow \forall y \in X A \subseteq ⋃ ⋃ ran g$
241	239 240	sylibr	$⊢ \forall y \in X A \subseteq ⋃ g (y) \to ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g$
242	234 241	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$
243	242	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$
244	232 243 228	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 ≼ ω))$
245		unieq	$⊢ z = ⋃ ran g \to ⋃ z = ⋃ ⋃ ran g$
246	245	sseq2d	$⊢ z = ⋃ ran g \to (⋃_{y \in X} A \subseteq ⋃ z \leftrightarrow ⋃_{y \in X} A \subseteq ⋃ ⋃ ran g)$
247		breq1	$⊢ z = ⋃ ran g \to (z ≼ ω \leftrightarrow ⋃ ran g ≼ ω)$
248	246 247	anbi12d	$⊢ z = ⋃ ran g \to ((⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω) \leftrightarrow (⋃_{y \in X} A \subseteq ⋃ ⋃ ran g \land ⋃ ran g ≼ ω))$
249	248	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 ≼ ω))$
250	244 249	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 ≼ ω)\}$
251		fveq2	$⊢ c = w \to R (c) = R (w)$
252	251	cbvesumv	$⊢ \underset{c \in ⋃ ran g}{\sum^{}} R (c) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)$
253		esumeq1	$⊢ x = ⋃ ran g \to \underset{w \in x}{\sum^{}} R (w) = \underset{w \in ⋃ ran g}{\sum^{}} R (w)$
254	253	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)$
255	250 252 254	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)$
256		esumex	$⊢ \underset{c \in ⋃ ran g}{\sum^{*}} R (c) \in V$
257		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))$
258	257	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))$
259	256 258	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)$
260	255 259	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))$
261	110	a1i	$⊢ φ \to < Or [0, +∞]$
262		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, +∞]$
263	2 3 173 262	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, +∞]$
264		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))$
265	263 264	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))$
266	261 265	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) < sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{}} R (w)) [0, +∞] <))$
267	1	fveq1i	$⊢ M (⋃_{y \in X} A) = toOMeas (R) (⋃_{y \in X} A)$
268	167 36	sseqtrd	$⊢ φ \to ⋃_{y \in X} A \subseteq ⋃ Q$
269		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land ⋃_{y \in X} A \subseteq ⋃ Q) \to toOMeas (R) (⋃_{y \in X} A) = sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
270	2 3 268 269	syl3anc	$⊢ φ \to toOMeas (R) (⋃_{y \in X} A) = sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
271	267 270	syl5eq	$⊢ φ \to M (⋃_{y \in X} A) = sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <)$
272	271	breq2d	$⊢ φ \to (\underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A) \leftrightarrow \underset{c \in ⋃ ran g}{\sum^{}} R (c) < sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <))$
273	272	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) < sup (ran (x \in \{z \in 𝒫 dom R \| (⋃_{y \in X} A \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{w \in x}{\sum^{*}} R (w)) [0, +∞] <))$
274	266 273	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))$
275	164 260 274	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)$
276		biid	$⊢ \neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A) \leftrightarrow \neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A)$
277	275 276	sylib	$⊢ (((((φ \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)$
278		xrlenlt	$⊢ (M (⋃_{y \in X} A) \in ℝ^{} \land \underset{c \in ⋃ ran g}{\sum^{}} R (c) \in ℝ^{}) \to (M (⋃_{y \in X} A) \leq \underset{c \in ⋃ ran g}{\sum^{}} R (c) \leftrightarrow \neg \underset{c \in ⋃ ran g}{\sum^{*}} R (c) < M (⋃_{y \in X} A))$
279	176 201 278	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 (M (⋃_{y \in X} A) \leq \underset{c \in ⋃ ran g}{\sum^{}} R (c) \leftrightarrow \neg \underset{c \in ⋃ ran g}{\sum^{}} R (c) < M (⋃_{y \in X} A))$
280	277 279	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 M (⋃_{y \in X} A) \leq \underset{c \in ⋃ ran g}{\sum^{*}} R (c)$
281		nfv	$⊢ Ⅎ y g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
282	26 281	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 ≼ ω\})$
283		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)}}))$
284	282 283	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)}})))$
285		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 φ$
286		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 ≼ ω\}$
287		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$
288	3	ad3antrrr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to R : Q ⟶ [0, +∞]$
289		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 ≼ ω\}$
290		simplr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to y \in X$
291	289 290	ffvelrnd	$⊢ (((φ \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 ≼ ω\}$
292	186 291	sselid	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \in 𝒫 dom R$
293	292	elpwid	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \subseteq dom R$
294	288 293	fssdmd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to g (y) \subseteq Q$
295		simpr	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to w \in g (y)$
296	294 295	sseldd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to w \in Q$
297	288 296	ffvelrnd	$⊢ (((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \land w \in g (y)) \to R (w) \in [0, +∞]$
298	297	ralrimiva	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \forall w \in g (y) R (w) \in [0, +∞]$
299		fvex	$⊢ g (y) \in V$
300		nfcv	$⊢ \underline{Ⅎ} w g (y)$
301	300	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, +∞]$
302	299 301	mpan	$⊢ \forall w \in g (y) R (w) \in [0, +∞] \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
303	298 302	syl	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞]$
304	285 286 287 303	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, +∞]$
305	304	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 \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 \to \underset{w \in g (y)}{\sum^{*}} R (w) \in [0, +∞])$
306	284 305	ralrimi	$⊢ (((((φ \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, +∞]$
307	18	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, +∞]$
308	178 306 307	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, +∞]$
309	105 308	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 ℝ^{*}$
310		nfv	$⊢ Ⅎ w (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\})$
311		simpr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}$
312		fniunfv	$⊢ g Fn X \to ⋃_{y \in X} g (y) = ⋃ ran g$
313	311 213 312	3syl	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to ⋃_{y \in X} g (y) = ⋃ ran g$
314	310 313	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)$
315	15	adantr	$⊢ (φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \to X \in V$
316	299	a1i	$⊢ ((φ \land g : X ⟶ \{z \in 𝒫 dom R \| z ≼ ω\}) \land y \in X) \to g (y) \in V$
317	315 316 297	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)$
318	314 317	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)$
319	13 318	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 ≼ ω\}) \to \underset{w \in ⋃ ran g}{\sum^{}} R (w) \leq \underset{y \in X}{\sum^{}} \underset{w \in g (y)}{\sum^{}} R (w)$
320	319	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)$
321	252 320	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)$
322	285 287 46	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, +∞]$
323		simplll	$⊢ ((((((φ \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 (((φ \land \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+})$
324	323 287 73	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 \frac{e}{2^{f (y)}} \in [0, +∞]$
325	322 324	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, +∞]$
326	325	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 \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 \to M (A) +_{𝑒} (\frac{e}{2^{f (y)}}) \in [0, +∞])$
327	284 326	ralrimi	$⊢ (((((φ \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, +∞]$
328	18	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, +∞]$
329	178 327 328	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, +∞]$
330	105 329	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 ℝ^{}$
331	215 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$
332		simp-4l	$⊢ (((((φ \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 (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ)$
333		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$
334	332 333 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 y \in X) \to M (A) \in ℝ$
335	334	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 ℝ$
336	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 ℝ$
337	336	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 ℝ$
338		id	$⊢ \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)}})$
339	338	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 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)}})$
340	66	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)}}))$
341	340	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)}})$
342	335 337 339 341	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)}})$
343	342	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)}}))$
344	332	simpld	$⊢ (((((φ \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 φ$
345		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 ≼ ω\}$
346	344 345 333 303	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, +∞]$
347	105 346	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 ℝ^{*}$
348	334	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 ℝ^{}$
349	336	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 ℝ^{}$
350	348 349	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 ℝ^{}$
351		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)}}))$
352	347 350 351	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)}}))$
353	343 352	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)}}))$
354	353	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)}}))$
355	354	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 ≼ ω\}) \to (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)}})))$
356	282 355	ralrimi	$⊢ ((((φ \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 \underset{w \in g (y)}{\sum^{*}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}}))$
357		ralim	$⊢ \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 g (y)}{\sum^{}} R (w) \leq M (A) +_{𝑒} (\frac{e}{2^{f (y)}})) \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)}}))$
358	356 357	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 ≼ ω\}) \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)}}))$
359	358	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)}})$
360	359	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)}})$
361	284 18 331 304 325 360	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)}}))$
362	164 46	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, +∞]$
363	284 18 331 362 324	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)}})$
364	324	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 \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 \to \frac{e}{2^{f (y)}} \in [0, +∞])$
365	284 364	ralrimi	$⊢ (((((φ \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, +∞]$
366	18	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, +∞]$
367	178 365 366	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, +∞]$
368	105 367	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 ℝ^{}$
369		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}{⟶} ℕ$
370		vex	$⊢ f \in V$
371	370	rnex	$⊢ ran f \in V$
372	371	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to ran f \in V$
373	58	frnd	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ran f \subseteq ℕ$
374	373	adantr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to ran f \subseteq ℕ$
375	374	sselda	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ran f) \to z \in ℕ$
376	54	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to 2 \in ℝ^{+}$
377		simpr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to z \in ℕ$
378	377	nnzd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to z \in ℤ$
379	376 378	rpexpcld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to 2^{z} \in ℝ^{+}$
380	379	rpreccld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in ℝ^{+}$
381	71 380	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞]$
382	381	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞]$
383	375 382	syldan	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land z \in ran f) \to \frac{1}{2^{z}} \in [0, +∞]$
384	383	ralrimiva	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \forall z \in ran f \frac{1}{2^{z}} \in [0, +∞]$
385		nfcv	$⊢ \underline{Ⅎ} z ran f$
386	385	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, +∞]$
387	372 384 386	syl2anc	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \in [0, +∞]$
388	105 387	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{}} (\frac{1}{2^{z}}) \in ℝ^{}$
389		1xr	$⊢ 1 \in ℝ^{*}$
390	389	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to 1 \in ℝ^{*}$
391	71	sseli	$⊢ e \in ℝ^{+} \to e \in [0, +∞]$
392	391	adantl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in [0, +∞]$
393		elxrge0	$⊢ e \in [0, +∞] \leftrightarrow (e \in ℝ^{*} \land 0 \leq e)$
394	392 393	sylib	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to (e \in ℝ^{*} \land 0 \leq e)$
395		nfv	$⊢ Ⅎ z (φ \land f : X \underset{1-1}{⟶} ℕ)$
396		nnex	$⊢ ℕ \in V$
397	396	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ℕ \in V$
398	395 397 381 373	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}})$
399		oveq2	$⊢ z = w \to 2^{z} = 2^{w}$
400	399	oveq2d	$⊢ z = w \to \frac{1}{2^{z}} = \frac{1}{2^{w}}$
401		ioossico	$⊢ (0, +∞) \subseteq [0, +∞)$
402	69 401	eqsstri	$⊢ ℝ^{+} \subseteq [0, +∞)$
403	402 380	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to \frac{1}{2^{z}} \in [0, +∞)$
404		eqidd	$⊢ z \in ℕ \to (w \in ℕ ⟼ \frac{1}{2^{w}}) = (w \in ℕ ⟼ \frac{1}{2^{w}})$
405		simpr	$⊢ (z \in ℕ \land w = z) \to w = z$
406	405	oveq2d	$⊢ (z \in ℕ \land w = z) \to 2^{w} = 2^{z}$
407	406	oveq2d	$⊢ (z \in ℕ \land w = z) \to \frac{1}{2^{w}} = \frac{1}{2^{z}}$
408		id	$⊢ z \in ℕ \to z \in ℕ$
409		ovexd	$⊢ z \in ℕ \to \frac{1}{2^{z}} \in V$
410	404 407 408 409	fvmptd	$⊢ z \in ℕ \to (w \in ℕ ⟼ \frac{1}{2^{w}}) (z) = \frac{1}{2^{z}}$
411	410	adantl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land z \in ℕ) \to (w \in ℕ ⟼ \frac{1}{2^{w}}) (z) = \frac{1}{2^{z}}$
412		ax-1cn	$⊢ 1 \in ℂ$
413		eqid	$⊢ (w \in ℕ ⟼ \frac{1}{2^{w}}) = (w \in ℕ ⟼ \frac{1}{2^{w}})$
414	413	geo2lim	$⊢ 1 \in ℂ \to seq 1 (+ (w \in ℕ ⟼ \frac{1}{2^{w}})) ⇝ 1$
415	412 414	ax-mp	$⊢ seq 1 (+ (w \in ℕ ⟼ \frac{1}{2^{w}})) ⇝ 1$
416	415	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to seq 1 (+ (w \in ℕ ⟼ \frac{1}{2^{w}})) ⇝ 1$
417		1re	$⊢ 1 \in ℝ$
418	417	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to 1 \in ℝ$
419	400 403 411 416 418	esumcvgsum	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ℕ}{\sum^{*}} (\frac{1}{2^{z}}) = \sum_{z \in ℕ} (\frac{1}{2^{z}})$
420		geoihalfsum	$⊢ \sum_{z \in ℕ} (\frac{1}{2^{z}}) = 1$
421	419 420	eqtrdi	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ℕ}{\sum^{*}} (\frac{1}{2^{z}}) = 1$
422	398 421	breqtrd	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \leq 1$
423	422	adantr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{z \in ran f}{\sum^{*}} (\frac{1}{2^{z}}) \leq 1$
424		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$
425	388 390 394 423 424	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$
426	17 23	nfan	$⊢ Ⅎ y (φ \land f : X \underset{1-1}{⟶} ℕ)$
427	426 25	nfan	$⊢ Ⅎ y ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+})$
428	76	recnd	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to e \in ℂ$
429	78	recnd	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \in ℂ$
430	429	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \in ℂ$
431		2cn	$⊢ 2 \in ℂ$
432	431	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \in ℂ$
433		2ne0	$⊢ 2 \neq 0$
434	433	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2 \neq 0$
435	432 434 60	expne0d	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 2^{f (y)} \neq 0$
436	435	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to 2^{f (y)} \neq 0$
437	428 430 436	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)}})$
438		1rp	$⊢ 1 \in ℝ^{+}$
439	438	a1i	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to 1 \in ℝ^{+}$
440	439 61	rpdivcld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ^{+}$
441	52 440	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ$
442	441	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{1}{2^{f (y)}} \in ℝ$
443		rexmul	$⊢ (e \in ℝ \land \frac{1}{2^{f (y)}} \in ℝ) \to e \cdot_{𝑒} (\frac{1}{2^{f (y)}}) = e (\frac{1}{2^{f (y)}})$
444	76 442 443	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)}})$
445	437 444	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)}})$
446	445	ralrimiva	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \forall y \in X \frac{e}{2^{f (y)}} = e \cdot_{𝑒} (\frac{1}{2^{f (y)}})$
447	427 446	esumeq2d	$⊢ ((φ \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)}}))$
448	15	ad2antrr	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to X \in V$
449	71 440	sselid	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land y \in X) \to \frac{1}{2^{f (y)}} \in [0, +∞]$
450	449	adantlr	$⊢ (((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \land y \in X) \to \frac{1}{2^{f (y)}} \in [0, +∞]$
451	402	a1i	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ℝ^{+} \subseteq [0, +∞)$
452	451	sselda	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in [0, +∞)$
453	448 450 452	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)}}))$
454		nfcv	$⊢ \underline{Ⅎ} y (\frac{1}{2^{z}})$
455		oveq2	$⊢ z = f (y) \to 2^{z} = 2^{f (y)}$
456	455	oveq2d	$⊢ z = f (y) \to \frac{1}{2^{z}} = \frac{1}{2^{f (y)}}$
457	15	adantr	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to X \in V$
458	56	simprbi	$⊢ f : X \underset{1-1}{⟶} ℕ \to Fun f^{-1}$
459	57	feqmptd	$⊢ f : X \underset{1-1}{⟶} ℕ \to f = (y \in X ⟼ f (y))$
460	459	cnveqd	$⊢ f : X \underset{1-1}{⟶} ℕ \to f^{-1} = {(y \in X ⟼ f (y))}^{-1}$
461	460	funeqd	$⊢ f : X \underset{1-1}{⟶} ℕ \to (Fun f^{-1} \leftrightarrow Fun {(y \in X ⟼ f (y))}^{-1})$
462	458 461	mpbid	$⊢ f : X \underset{1-1}{⟶} ℕ \to Fun {(y \in X ⟼ f (y))}^{-1}$
463	462	adantl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to Fun {(y \in X ⟼ f (y))}^{-1}$
464	454 426 18 456 457 463 449 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}})$
465		ffn	$⊢ f : X ⟶ ℕ \to f Fn X$
466		fnrnfv	$⊢ f Fn X \to ran f = \{x \| \exists y \in X x = f (y)\}$
467	58 465 466	3syl	$⊢ (φ \land f : X \underset{1-1}{⟶} ℕ) \to ran f = \{x \| \exists y \in X x = f (y)\}$
468	395 467	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}})$
469	464 468	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}})$
470	469	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}})$
471	470	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}})$
472	447 453 471	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)}})$
473	394	simpld	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \in ℝ^{*}$
474		xmulid1	$⊢ e \in ℝ^{*} \to e \cdot_{𝑒} 1 = e$
475	473 474	syl	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to e \cdot_{𝑒} 1 = e$
476	425 472 475	3brtr3d	$⊢ ((φ \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to \underset{y \in X}{\sum^{*}} (\frac{e}{2^{f (y)}}) \leq e$
477	164 369 204 476	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$
478		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$
479	368 205 203 477 478	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$
480	363 479	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$
481	309 330 206 361 480	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$
482	201 309 206 321 481	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$
483	176 201 206 280 482	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$
484	204	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 ℝ$
485		rexadd	$⊢ (\underset{y \in X}{\sum^{}} M (A) \in ℝ \land e \in ℝ) \to \underset{y \in X}{\sum^{}} M (A) +_{𝑒} e = \underset{y \in X}{\sum^{*}} M (A) + e$
486	202 484 485	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) +_{𝑒} e = \underset{y \in X}{\sum^{}} M (A) + e$
487	483 486	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$
488	487	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$
489	488	ex	$⊢ (((φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \land f : X \underset{1-1}{⟶} ℕ) \land e \in ℝ^{+}) \to ((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)$
490	489	exlimdv	$⊢ (((φ \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)}}))) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A) + e)$
491	163 490	mpd	$⊢ (((φ \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$
492	491	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$
493		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)$
494	175 493	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)$
495	494	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)$
496	492 495	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)$
497	496	ex	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to (f : X \underset{1-1}{⟶} ℕ \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A))$
498	497	exlimdv	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to (\exists f f : X \underset{1-1}{⟶} ℕ \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A))$
499	12 498	mpd	$⊢ (φ \land \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{}} M (A)$
500	175	adantr	$⊢ (φ \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \in ℝ^{}$
501		pnfge	$⊢ M (⋃_{y \in X} A) \in ℝ^{*} \to M (⋃_{y \in X} A) \leq +∞$
502	500 501	syl	$⊢ (φ \land \neg \underset{y \in X}{\sum^{*}} M (A) \in ℝ) \to M (⋃_{y \in X} A) \leq +∞$
503	46	ralrimiva	$⊢ φ \to \forall y \in X M (A) \in [0, +∞]$
504	18	esumcl	$⊢ (X \in V \land \forall y \in X M (A) \in [0, +∞]) \to \underset{y \in X}{\sum^{*}} M (A) \in [0, +∞]$
505	15 503 504	syl2anc	$⊢ φ \to \underset{y \in X}{\sum^{*}} M (A) \in [0, +∞]$
506		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) = +∞$
507	505 506	sylan	$⊢ (φ \land \neg \underset{y \in X}{\sum^{}} M (A) \in ℝ) \to \underset{y \in X}{\sum^{}} M (A) = +∞$
508	502 507	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)$
509	499 508	pm2.61dan	$⊢ φ \to M (⋃_{y \in X} A) \leq \underset{y \in X}{\sum^{*}} M (A)$

Metamath Proof Explorer

Theorem omssubadd

Proof