ovnsubadd

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

	Ref	Expression
Hypotheses	ovnsubadd.1	$⊢ φ \to X \in Fin$
	ovnsubadd.2	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
Assertion	ovnsubadd	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd.1	$⊢ φ \to X \in Fin$
2		ovnsubadd.2	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
3		fveq2	$⊢ X = \emptyset \to voln* (X) = voln* (\emptyset)$
4	3	fveq1d	$⊢ X = \emptyset \to voln* (X) (⋃_{n \in ℕ} A (n)) = voln* (\emptyset) (⋃_{n \in ℕ} A (n))$
5	4	adantl	$⊢ (φ \land X = \emptyset) \to voln* (X) (⋃_{n \in ℕ} A (n)) = voln* (\emptyset) (⋃_{n \in ℕ} A (n))$
6	2	adantr	$⊢ (φ \land n \in ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
7		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
8	6 7	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to A (n) \in 𝒫 (ℝ^{X})$
9		elpwi	$⊢ A (n) \in 𝒫 (ℝ^{X}) \to A (n) \subseteq ℝ^{X}$
10	8 9	syl	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ℝ^{X}$
11	10	ralrimiva	$⊢ φ \to \forall n \in ℕ A (n) \subseteq ℝ^{X}$
12		iunss	$⊢ ⋃_{n \in ℕ} A (n) \subseteq ℝ^{X} \leftrightarrow \forall n \in ℕ A (n) \subseteq ℝ^{X}$
13	11 12	sylibr	$⊢ φ \to ⋃_{n \in ℕ} A (n) \subseteq ℝ^{X}$
14	13	adantr	$⊢ (φ \land X = \emptyset) \to ⋃_{n \in ℕ} A (n) \subseteq ℝ^{X}$
15		oveq2	$⊢ X = \emptyset \to ℝ^{X} = ℝ^{\emptyset}$
16	15	adantl	$⊢ (φ \land X = \emptyset) \to ℝ^{X} = ℝ^{\emptyset}$
17	14 16	sseqtrd	$⊢ (φ \land X = \emptyset) \to ⋃_{n \in ℕ} A (n) \subseteq ℝ^{\emptyset}$
18	17	ovn0val	$⊢ (φ \land X = \emptyset) \to voln* (\emptyset) (⋃_{n \in ℕ} A (n)) = 0$
19	5 18	eqtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (⋃_{n \in ℕ} A (n)) = 0$
20		nnex	$⊢ ℕ \in V$
21	20	a1i	$⊢ φ \to ℕ \in V$
22	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
23	22 10	ovncl	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) \in [0, +∞]$
24		eqid	$⊢ (n \in ℕ ⟼ voln* (X) (A (n))) = (n \in ℕ ⟼ voln* (X) (A (n)))$
25	23 24	fmptd	$⊢ φ \to (n \in ℕ ⟼ voln* (X) (A (n))) : ℕ ⟶ [0, +∞]$
26	21 25	sge0ge0	$⊢ φ \to 0 \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$
27	26	adantr	$⊢ (φ \land X = \emptyset) \to 0 \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$
28	19 27	eqbrtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$
29	1 13	ovnxrcl	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \in ℝ^{*}$
30	29	adantr	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (⋃_{n \in ℕ} A (n)) \in ℝ^{*}$
31	21 25	sge0xrcl	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (A (n)))) \in ℝ^{*}$
32	31	adantr	$⊢ (φ \land \neg X = \emptyset) \to sum^((n \in ℕ ⟼ voln* (X) (A (n)))) \in ℝ^{*}$
33	1	ad2antrr	$⊢ ((φ \land \neg X = \emptyset) \land y \in ℝ^{+}) \to X \in Fin$
34		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
35	34	ad2antlr	$⊢ ((φ \land \neg X = \emptyset) \land y \in ℝ^{+}) \to X \neq \emptyset$
36	2	ad2antrr	$⊢ ((φ \land \neg X = \emptyset) \land y \in ℝ^{+}) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
37		simpr	$⊢ ((φ \land \neg X = \emptyset) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
38		eqid	$⊢ (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)))))\}) = (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)))))\})$
39		sseq1	$⊢ b = a \to (b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) \leftrightarrow a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k))$
40	39	rabbidv	$⊢ b = a \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
41	40	cbvmptv	$⊢ (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
42		eqid	$⊢ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
43		fveq2	$⊢ o = j \to l (o) = l (j)$
44	43	coeq2d	$⊢ o = j \to [.) \circ l (o) = [.) \circ l (j)$
45	44	fveq1d	$⊢ o = j \to ([.) \circ l (o)) (d) = ([.) \circ l (j)) (d)$
46	45	ixpeq2dv	$⊢ o = j \to \underset{d \in X}{⨉} ([.) \circ l (o)) (d) = \underset{d \in X}{⨉} ([.) \circ l (j)) (d)$
47		fveq2	$⊢ d = k \to ([.) \circ l (j)) (d) = ([.) \circ l (j)) (k)$
48	47	cbvixpv	$⊢ \underset{d \in X}{⨉} ([.) \circ l (j)) (d) = \underset{k \in X}{⨉} ([.) \circ l (j)) (k)$
49	46 48	eqtrdi	$⊢ o = j \to \underset{d \in X}{⨉} ([.) \circ l (o)) (d) = \underset{k \in X}{⨉} ([.) \circ l (j)) (k)$
50	49	cbviunv	$⊢ ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)$
51	50	sseq2i	$⊢ b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d) \leftrightarrow b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)$
52	51	rabbii	$⊢ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\} = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
53	52	mpteq2i	$⊢ (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) = (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
54	53	fveq1i	$⊢ (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) = (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (d)$
55		fveq2	$⊢ d = a \to (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (d) = (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a)$
56	54 55	eqtrid	$⊢ d = a \to (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) = (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a)$
57	56	eleq2d	$⊢ d = a \to (m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \leftrightarrow m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a))$
58		2fveq3	$⊢ d = k \to vol (([.) \circ h) (d)) = vol (([.) \circ h) (k))$
59	58	cbvprodv	$⊢ \prod_{d \in X} vol (([.) \circ h) (d)) = \prod_{k \in X} vol (([.) \circ h) (k))$
60	59	mpteq2i	$⊢ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
61	60	a1i	$⊢ o = j \to (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
62		fveq2	$⊢ o = j \to m (o) = m (j)$
63	61 62	fveq12d	$⊢ o = j \to (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j))$
64	63	cbvmptv	$⊢ (o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o))) = (j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))$
65	64	fveq2i	$⊢ sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) = sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j))))$
66	65	a1i	$⊢ d = a \to sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) = sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j))))$
67		fveq2	$⊢ d = a \to voln* (X) (d) = voln* (X) (a)$
68	67	oveq1d	$⊢ d = a \to voln* (X) (d) +_{𝑒} f = voln* (X) (a) +_{𝑒} f$
69	66 68	breq12d	$⊢ d = a \to (sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f \leftrightarrow sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) \leq voln* (X) (a) +_{𝑒} f)$
70	57 69	anbi12d	$⊢ d = a \to ((m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \land sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f) \leftrightarrow (m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \land sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) \leq voln* (X) (a) +_{𝑒} f))$
71	70	rabbidva2	$⊢ d = a \to \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \| sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f\} = \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) \leq voln* (X) (a) +_{𝑒} f\}$
72		fveq1	$⊢ m = i \to m (j) = i (j)$
73	72	fveq2d	$⊢ m = i \to (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)) = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j))$
74	73	mpteq2dv	$⊢ m = i \to (j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j))) = (j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))$
75	74	fveq2d	$⊢ m = i \to sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) = sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j))))$
76	75	breq1d	$⊢ m = i \to (sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) \leq voln* (X) (a) +_{𝑒} f \leftrightarrow sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f)$
77	76	cbvrabv	$⊢ \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (m (j)))) \leq voln* (X) (a) +_{𝑒} f\} = \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f\}$
78	71 77	eqtrdi	$⊢ d = a \to \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \| sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f\} = \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f\}$
79	78	mpteq2dv	$⊢ d = a \to (f \in ℝ^{+} ⟼ \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \| sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f\}) = (f \in ℝ^{+} ⟼ \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f\})$
80		oveq2	$⊢ f = e \to voln* (X) (a) +_{𝑒} f = voln* (X) (a) +_{𝑒} e$
81	80	breq2d	$⊢ f = e \to (sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f \leftrightarrow sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} e)$
82	81	rabbidv	$⊢ f = e \to \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f\} = \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}$
83	82	cbvmptv	$⊢ (f \in ℝ^{+} ⟼ \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} f\}) = (e \in ℝ^{+} ⟼ \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} e\})$
84	79 83	eqtrdi	$⊢ d = a \to (f \in ℝ^{+} ⟼ \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \| sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f\}) = (e \in ℝ^{+} ⟼ \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} e\})$
85	84	cbvmptv	$⊢ (d \in 𝒫 (ℝ^{X}) ⟼ (f \in ℝ^{+} ⟼ \{m \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{o \in ℕ} \underset{d \in X}{⨉} ([.) \circ l (o)) (d)\}) (d) \| sum^((o \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{d \in X} vol (([.) \circ h) (d))) (m (o)))) \leq voln* (X) (d) +_{𝑒} f\})) = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in (b \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| b \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}) (a) \| sum^((j \in ℕ ⟼ (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k))) (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
86	33 35 36 37 38 41 42 85	ovnsubaddlem2	$⊢ ((φ \land \neg X = \emptyset) \land y \in ℝ^{+}) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} y$
87	30 32 86	xrlexaddrp	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$
88	28 87	pm2.61dan	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n))))$

Metamath Proof Explorer

Theorem ovnsubadd

Proof