ovnsubaddlem2

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsubaddlem2.x	$⊢ φ \to X \in Fin$
	ovnsubaddlem2.n0	$⊢ φ \to X \neq \emptyset$
	ovnsubaddlem2.a	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
	ovnsubaddlem2.e	$⊢ φ \to E \in ℝ^{+}$
	ovnsubaddlem2.z	$⊢ Z = (a \in 𝒫 (ℝ^{X}) ⟼ \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\})$
	ovnsubaddlem2.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
	ovnsubaddlem2.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
	ovnsubaddlem2.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
Assertion	ovnsubaddlem2	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$

Proof

Step	Hyp	Ref	Expression
1		ovnsubaddlem2.x	$⊢ φ \to X \in Fin$
2		ovnsubaddlem2.n0	$⊢ φ \to X \neq \emptyset$
3		ovnsubaddlem2.a	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
4		ovnsubaddlem2.e	$⊢ φ \to E \in ℝ^{+}$
5		ovnsubaddlem2.z	$⊢ Z = (a \in 𝒫 (ℝ^{X}) ⟼ \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\})$
6		ovnsubaddlem2.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
7		ovnsubaddlem2.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
8		ovnsubaddlem2.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
9		fvex	$⊢ D (A (n)) (\frac{E}{2^{n}}) \in V$
10		nnenom	$⊢ ℕ \approx ω$
11	9 10	axcc3	$⊢ \exists g (g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})))$
12		simprl	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})))) \to g Fn ℕ$
13		nfv	$⊢ Ⅎ n φ$
14		nfra1	$⊢ Ⅎ n \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
15	13 14	nfan	$⊢ Ⅎ n (φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})))$
16		rspa	$⊢ (\forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land n \in ℕ) \to (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
17	16	adantll	$⊢ ((φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \land n \in ℕ) \to (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
18	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
19	2	adantr	$⊢ (φ \land n \in ℕ) \to X \neq \emptyset$
20	3	adantr	$⊢ (φ \land n \in ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
21		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
22	20 21	ffvelrnd	$⊢ (φ \land n \in ℕ) \to A (n) \in 𝒫 (ℝ^{X})$
23		elpwi	$⊢ A (n) \in 𝒫 (ℝ^{X}) \to A (n) \subseteq ℝ^{X}$
24	22 23	syl	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ℝ^{X}$
25	4	adantr	$⊢ (φ \land n \in ℕ) \to E \in ℝ^{+}$
26		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
27		2nn	$⊢ 2 \in ℕ$
28	27	a1i	$⊢ n \in ℕ_{0} \to 2 \in ℕ$
29		id	$⊢ n \in ℕ_{0} \to n \in ℕ_{0}$
30		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
31	28 29 30	syl2anc	$⊢ n \in ℕ_{0} \to 2^{n} \in ℕ$
32		nnrp	$⊢ 2^{n} \in ℕ \to 2^{n} \in ℝ^{+}$
33	31 32	syl	$⊢ n \in ℕ_{0} \to 2^{n} \in ℝ^{+}$
34	26 33	syl	$⊢ n \in ℕ \to 2^{n} \in ℝ^{+}$
35	34	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ^{+}$
36	25 35	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \in ℝ^{+}$
37	18 19 24 36 6 7 8	ovncvrrp	$⊢ (φ \land n \in ℕ) \to \exists i i \in D (A (n)) (\frac{E}{2^{n}})$
38		n0	$⊢ D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \leftrightarrow \exists i i \in D (A (n)) (\frac{E}{2^{n}})$
39	37 38	sylibr	$⊢ (φ \land n \in ℕ) \to D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset$
40	39	adantr	$⊢ ((φ \land n \in ℕ) \land (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset$
41		simpr	$⊢ ((φ \land n \in ℕ) \land (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
42	40 41	mpd	$⊢ ((φ \land n \in ℕ) \land (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to g (n) \in D (A (n)) (\frac{E}{2^{n}})$
43	42	ex	$⊢ (φ \land n \in ℕ) \to ((D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
44	43	adantlr	$⊢ ((φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \land n \in ℕ) \to ((D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
45	17 44	mpd	$⊢ ((φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \land n \in ℕ) \to g (n) \in D (A (n)) (\frac{E}{2^{n}})$
46	45	ex	$⊢ (φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to (n \in ℕ \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
47	15 46	ralrimi	$⊢ (φ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
48	47	adantrl	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})))) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
49	12 48	jca	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}})))) \to (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
50	49	ex	$⊢ φ \to ((g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})))$
51	50	eximdv	$⊢ φ \to (\exists g (g Fn ℕ \land \forall n \in ℕ (D (A (n)) (\frac{E}{2^{n}}) \neq \emptyset \to g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to \exists g (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})))$
52	11 51	mpi	$⊢ φ \to \exists g (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
53		simpl	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to φ$
54		simprl	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to g Fn ℕ$
55		simprr	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
56		nnf1oxpnn	$⊢ \exists f f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
57		simpl1	$⊢ ((φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to φ$
58		simpl2	$⊢ ((φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to g Fn ℕ$
59		fveq2	$⊢ q = n \to g (q) = g (n)$
60		2fveq3	$⊢ q = n \to D (A (q)) = D (A (n))$
61		oveq2	$⊢ q = n \to 2^{q} = 2^{n}$
62	61	oveq2d	$⊢ q = n \to \frac{E}{2^{q}} = \frac{E}{2^{n}}$
63	60 62	fveq12d	$⊢ q = n \to D (A (q)) (\frac{E}{2^{q}}) = D (A (n)) (\frac{E}{2^{n}})$
64	59 63	eleq12d	$⊢ q = n \to (g (q) \in D (A (q)) (\frac{E}{2^{q}}) \leftrightarrow g (n) \in D (A (n)) (\frac{E}{2^{n}}))$
65	64	cbvralvw	$⊢ \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}}) \leftrightarrow \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
66	65	biimpri	$⊢ \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}) \to \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})$
67	66	3ad2ant3	$⊢ (φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})$
68	67	adantr	$⊢ ((φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})$
69		simpr	$⊢ ((φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
70	1	adantr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to X \in Fin$
71	70	3ad2antl1	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to X \in Fin$
72	2	adantr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to X \neq \emptyset$
73	72	3ad2antl1	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to X \neq \emptyset$
74	3	adantr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
75	74	3ad2antl1	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
76	4	adantr	$⊢ (φ \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to E \in ℝ^{+}$
77	76	3ad2antl1	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to E \in ℝ^{+}$
78		coeq2	$⊢ h = i \to [.) \circ h = [.) \circ i$
79	78	fveq1d	$⊢ h = i \to ([.) \circ h) (k) = ([.) \circ i) (k)$
80	79	fveq2d	$⊢ h = i \to vol (([.) \circ h) (k)) = vol (([.) \circ i) (k))$
81	80	prodeq2ad	$⊢ h = i \to \prod_{k \in X} vol (([.) \circ h) (k)) = \prod_{k \in X} vol (([.) \circ i) (k))$
82	81	cbvmptv	$⊢ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
83	7 82	eqtri	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
84	65	biimpi	$⊢ \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}}) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
85	84	3ad2ant3	$⊢ (φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
86	85	ad2antrr	$⊢ (((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \land n \in ℕ) \to \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})$
87		simpr	$⊢ (((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \land n \in ℕ) \to n \in ℕ$
88		rspa	$⊢ (\forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}) \land n \in ℕ) \to g (n) \in D (A (n)) (\frac{E}{2^{n}})$
89	86 87 88	syl2anc	$⊢ (((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \land n \in ℕ) \to g (n) \in D (A (n)) (\frac{E}{2^{n}})$
90		simpr	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
91		2fveq3	$⊢ q = m \to 1^{st} (f (q)) = 1^{st} (f (m))$
92	91	fveq2d	$⊢ q = m \to g (1^{st} (f (q))) = g (1^{st} (f (m)))$
93		2fveq3	$⊢ q = m \to 2^{nd} (f (q)) = 2^{nd} (f (m))$
94	92 93	fveq12d	$⊢ q = m \to g (1^{st} (f (q))) (2^{nd} (f (q))) = g (1^{st} (f (m))) (2^{nd} (f (m)))$
95	94	cbvmptv	$⊢ (q \in ℕ ⟼ g (1^{st} (f (q))) (2^{nd} (f (q)))) = (m \in ℕ ⟼ g (1^{st} (f (m))) (2^{nd} (f (m))))$
96	71 73 75 77 5 6 83 8 89 90 95	ovnsubaddlem1	$⊢ ((φ \land g Fn ℕ \land \forall q \in ℕ g (q) \in D (A (q)) (\frac{E}{2^{q}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
97	57 58 68 69 96	syl31anc	$⊢ ((φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \land f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
98	97	ex	$⊢ (φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to (f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E)$
99	98	exlimdv	$⊢ (φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to (\exists f f : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E)$
100	56 99	mpi	$⊢ (φ \land g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
101	53 54 55 100	syl3anc	$⊢ (φ \land (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}}))) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
102	101	ex	$⊢ φ \to ((g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E)$
103	102	exlimdv	$⊢ φ \to (\exists g (g Fn ℕ \land \forall n \in ℕ g (n) \in D (A (n)) (\frac{E}{2^{n}})) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E)$
104	52 103	mpd	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$

Metamath Proof Explorer

Theorem ovnsubaddlem2

Proof