ovnsubaddlem1

Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsubaddlem1.x	$⊢ φ \to X \in Fin$
	ovnsubaddlem1.n0	$⊢ φ \to X \neq \emptyset$
	ovnsubaddlem1.a	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
	ovnsubaddlem1.e	$⊢ φ \to E \in ℝ^{+}$
	ovnsubaddlem1.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)))))\})$
	ovnsubaddlem1.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\})$
	ovnsubaddlem1.l	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
	ovnsubaddlem1.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
	ovnsubaddlem1.i	$⊢ (φ \land n \in ℕ) \to I (n) \in D (A (n)) (\frac{E}{2^{n}})$
	ovnsubaddlem1.f	$⊢ φ \to F : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
	ovnsubaddlem1.g	$⊢ G = (m \in ℕ ⟼ I (1^{st} (F (m))) (2^{nd} (F (m))))$
Assertion	ovnsubaddlem1	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$

Proof

Step	Hyp	Ref	Expression
1		ovnsubaddlem1.x	$⊢ φ \to X \in Fin$
2		ovnsubaddlem1.n0	$⊢ φ \to X \neq \emptyset$
3		ovnsubaddlem1.a	$⊢ φ \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
4		ovnsubaddlem1.e	$⊢ φ \to E \in ℝ^{+}$
5		ovnsubaddlem1.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		ovnsubaddlem1.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\})$
7		ovnsubaddlem1.l	$⊢ L = (i \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ i) (k)))$
8		ovnsubaddlem1.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
9		ovnsubaddlem1.i	$⊢ (φ \land n \in ℕ) \to I (n) \in D (A (n)) (\frac{E}{2^{n}})$
10		ovnsubaddlem1.f	$⊢ φ \to F : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
11		ovnsubaddlem1.g	$⊢ G = (m \in ℕ ⟼ I (1^{st} (F (m))) (2^{nd} (F (m))))$
12	3	adantr	$⊢ (φ \land n \in ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
13		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
14	12 13	ffvelrnd	$⊢ (φ \land n \in ℕ) \to A (n) \in 𝒫 (ℝ^{X})$
15		elpwi	$⊢ A (n) \in 𝒫 (ℝ^{X}) \to A (n) \subseteq ℝ^{X}$
16	14 15	syl	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ℝ^{X}$
17	16	ralrimiva	$⊢ φ \to \forall n \in ℕ A (n) \subseteq ℝ^{X}$
18		iunss	$⊢ ⋃_{n \in ℕ} A (n) \subseteq ℝ^{X} \leftrightarrow \forall n \in ℕ A (n) \subseteq ℝ^{X}$
19	17 18	sylibr	$⊢ φ \to ⋃_{n \in ℕ} A (n) \subseteq ℝ^{X}$
20	1 19	ovnxrcl	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \in ℝ^{*}$
21		nfv	$⊢ Ⅎ m φ$
22		nnex	$⊢ ℕ \in V$
23	22	a1i	$⊢ φ \to ℕ \in V$
24		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
25		nfv	$⊢ Ⅎ k (φ \land m \in ℕ)$
26		simpl	$⊢ (φ \land m \in ℕ) \to φ$
27	26 1	syl	$⊢ (φ \land m \in ℕ) \to X \in Fin$
28		f1of	$⊢ F : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to F : ℕ ⟶ ℕ \times ℕ$
29	10 28	syl	$⊢ φ \to F : ℕ ⟶ ℕ \times ℕ$
30	29	adantr	$⊢ (φ \land m \in ℕ) \to F : ℕ ⟶ ℕ \times ℕ$
31		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
32	30 31	ffvelrnd	$⊢ (φ \land m \in ℕ) \to F (m) \in (ℕ \times ℕ)$
33		xp1st	$⊢ F (m) \in (ℕ \times ℕ) \to 1^{st} (F (m)) \in ℕ$
34	32 33	syl	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) \in ℕ$
35		xp2nd	$⊢ F (m) \in (ℕ \times ℕ) \to 2^{nd} (F (m)) \in ℕ$
36	32 35	syl	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) \in ℕ$
37		fvex	$⊢ 2^{nd} (F (m)) \in V$
38		eleq1	$⊢ j = 2^{nd} (F (m)) \to (j \in ℕ \leftrightarrow 2^{nd} (F (m)) \in ℕ)$
39	38	3anbi3d	$⊢ j = 2^{nd} (F (m)) \to ((φ \land 1^{st} (F (m)) \in ℕ \land j \in ℕ) \leftrightarrow (φ \land 1^{st} (F (m)) \in ℕ \land 2^{nd} (F (m)) \in ℕ))$
40		fveq2	$⊢ j = 2^{nd} (F (m)) \to I (1^{st} (F (m))) (j) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
41	40	feq1d	$⊢ j = 2^{nd} (F (m)) \to (I (1^{st} (F (m))) (j) : X ⟶ ℝ^{2} \leftrightarrow I (1^{st} (F (m))) (2^{nd} (F (m))) : X ⟶ ℝ^{2})$
42	39 41	imbi12d	$⊢ j = 2^{nd} (F (m)) \to (((φ \land 1^{st} (F (m)) \in ℕ \land j \in ℕ) \to I (1^{st} (F (m))) (j) : X ⟶ ℝ^{2}) \leftrightarrow ((φ \land 1^{st} (F (m)) \in ℕ \land 2^{nd} (F (m)) \in ℕ) \to I (1^{st} (F (m))) (2^{nd} (F (m))) : X ⟶ ℝ^{2}))$
43		fvex	$⊢ 1^{st} (F (m)) \in V$
44		eleq1	$⊢ n = 1^{st} (F (m)) \to (n \in ℕ \leftrightarrow 1^{st} (F (m)) \in ℕ)$
45	44	3anbi2d	$⊢ n = 1^{st} (F (m)) \to ((φ \land n \in ℕ \land j \in ℕ) \leftrightarrow (φ \land 1^{st} (F (m)) \in ℕ \land j \in ℕ))$
46		fveq2	$⊢ n = 1^{st} (F (m)) \to I (n) = I (1^{st} (F (m)))$
47	46	fveq1d	$⊢ n = 1^{st} (F (m)) \to I (n) (j) = I (1^{st} (F (m))) (j)$
48	47	feq1d	$⊢ n = 1^{st} (F (m)) \to (I (n) (j) : X ⟶ ℝ^{2} \leftrightarrow I (1^{st} (F (m))) (j) : X ⟶ ℝ^{2})$
49	45 48	imbi12d	$⊢ n = 1^{st} (F (m)) \to (((φ \land n \in ℕ \land j \in ℕ) \to I (n) (j) : X ⟶ ℝ^{2}) \leftrightarrow ((φ \land 1^{st} (F (m)) \in ℕ \land j \in ℕ) \to I (1^{st} (F (m))) (j) : X ⟶ ℝ^{2}))$
50		sseq1	$⊢ a = A (n) \to (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \leftrightarrow A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k))$
51	50	rabbidv	$⊢ a = A (n) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
52		ovex	$⊢ {({ℝ^{2}}^{X})}^{ℕ} \in V$
53	52	rabex	$⊢ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \in V$
54	53	a1i	$⊢ (φ \land n \in ℕ) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \in V$
55	6 51 14 54	fvmptd3	$⊢ (φ \land n \in ℕ) \to C (A (n)) = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
56		ssrab2	$⊢ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
57	56	a1i	$⊢ (φ \land n \in ℕ) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
58	55 57	eqsstrd	$⊢ (φ \land n \in ℕ) \to C (A (n)) \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
59		fveq2	$⊢ a = A (n) \to C (a) = C (A (n))$
60	59	eleq2d	$⊢ a = A (n) \to (i \in C (a) \leftrightarrow i \in C (A (n)))$
61		fveq2	$⊢ a = A (n) \to voln* (X) (a) = voln* (X) (A (n))$
62	61	oveq1d	$⊢ a = A (n) \to voln* (X) (a) +_{𝑒} e = voln* (X) (A (n)) +_{𝑒} e$
63	62	breq2d	$⊢ a = A (n) \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e)$
64	60 63	anbi12d	$⊢ a = A (n) \to ((i \in C (a) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e) \leftrightarrow (i \in C (A (n)) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e))$
65	64	rabbidva2	$⊢ a = A (n) \to \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\} = \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\}$
66	65	mpteq2dv	$⊢ a = A (n) \to (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}) = (e \in ℝ^{+} ⟼ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\})$
67		rpex	$⊢ ℝ^{+} \in V$
68	67	mptex	$⊢ (e \in ℝ^{+} ⟼ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\}) \in V$
69	68	a1i	$⊢ (φ \land n \in ℕ) \to (e \in ℝ^{+} ⟼ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\}) \in V$
70	8 66 14 69	fvmptd3	$⊢ (φ \land n \in ℕ) \to D (A (n)) = (e \in ℝ^{+} ⟼ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\})$
71		oveq2	$⊢ e = \frac{E}{2^{n}} \to voln* (X) (A (n)) +_{𝑒} e = voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})$
72	71	breq2d	$⊢ e = \frac{E}{2^{n}} \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))$
73	72	rabbidv	$⊢ e = \frac{E}{2^{n}} \to \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\} = \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\}$
74	73	adantl	$⊢ ((φ \land n \in ℕ) \land e = \frac{E}{2^{n}}) \to \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} e\} = \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\}$
75	4	adantr	$⊢ (φ \land n \in ℕ) \to E \in ℝ^{+}$
76		2nn	$⊢ 2 \in ℕ$
77	76	a1i	$⊢ n \in ℕ \to 2 \in ℕ$
78		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
79	77 78	nnexpcld	$⊢ n \in ℕ \to 2^{n} \in ℕ$
80	79	nnrpd	$⊢ n \in ℕ \to 2^{n} \in ℝ^{+}$
81	80	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ^{+}$
82	75 81	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \in ℝ^{+}$
83		fvex	$⊢ C (A (n)) \in V$
84	83	rabex	$⊢ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\} \in V$
85	84	a1i	$⊢ (φ \land n \in ℕ) \to \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\} \in V$
86	70 74 82 85	fvmptd	$⊢ (φ \land n \in ℕ) \to D (A (n)) (\frac{E}{2^{n}}) = \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\}$
87		ssrab2	$⊢ \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\} \subseteq C (A (n))$
88	87	a1i	$⊢ (φ \land n \in ℕ) \to \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\} \subseteq C (A (n))$
89	86 88	eqsstrd	$⊢ (φ \land n \in ℕ) \to D (A (n)) (\frac{E}{2^{n}}) \subseteq C (A (n))$
90	89 9	sseldd	$⊢ (φ \land n \in ℕ) \to I (n) \in C (A (n))$
91	58 90	sseldd	$⊢ (φ \land n \in ℕ) \to I (n) \in ({({ℝ^{2}}^{X})}^{ℕ})$
92		elmapfn	$⊢ I (n) \in ({({ℝ^{2}}^{X})}^{ℕ}) \to I (n) Fn ℕ$
93	91 92	syl	$⊢ (φ \land n \in ℕ) \to I (n) Fn ℕ$
94		elmapi	$⊢ I (n) \in ({({ℝ^{2}}^{X})}^{ℕ}) \to I (n) : ℕ ⟶ {ℝ^{2}}^{X}$
95	91 94	syl	$⊢ (φ \land n \in ℕ) \to I (n) : ℕ ⟶ {ℝ^{2}}^{X}$
96	95	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to I (n) (j) \in ({ℝ^{2}}^{X})$
97	96	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall j \in ℕ I (n) (j) \in ({ℝ^{2}}^{X})$
98	93 97	jca	$⊢ (φ \land n \in ℕ) \to (I (n) Fn ℕ \land \forall j \in ℕ I (n) (j) \in ({ℝ^{2}}^{X}))$
99	98	3adant3	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to (I (n) Fn ℕ \land \forall j \in ℕ I (n) (j) \in ({ℝ^{2}}^{X}))$
100		ffnfv	$⊢ I (n) : ℕ ⟶ {ℝ^{2}}^{X} \leftrightarrow (I (n) Fn ℕ \land \forall j \in ℕ I (n) (j) \in ({ℝ^{2}}^{X}))$
101	99 100	sylibr	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to I (n) : ℕ ⟶ {ℝ^{2}}^{X}$
102		simp3	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to j \in ℕ$
103	101 102	ffvelrnd	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to I (n) (j) \in ({ℝ^{2}}^{X})$
104		elmapi	$⊢ I (n) (j) \in ({ℝ^{2}}^{X}) \to I (n) (j) : X ⟶ ℝ^{2}$
105	103 104	syl	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to I (n) (j) : X ⟶ ℝ^{2}$
106	43 49 105	vtocl	$⊢ (φ \land 1^{st} (F (m)) \in ℕ \land j \in ℕ) \to I (1^{st} (F (m))) (j) : X ⟶ ℝ^{2}$
107	37 42 106	vtocl	$⊢ (φ \land 1^{st} (F (m)) \in ℕ \land 2^{nd} (F (m)) \in ℕ) \to I (1^{st} (F (m))) (2^{nd} (F (m))) : X ⟶ ℝ^{2}$
108	26 34 36 107	syl3anc	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) (2^{nd} (F (m))) : X ⟶ ℝ^{2}$
109		id	$⊢ m \in ℕ \to m \in ℕ$
110		fvex	$⊢ I (1^{st} (F (m))) (2^{nd} (F (m))) \in V$
111	110	a1i	$⊢ m \in ℕ \to I (1^{st} (F (m))) (2^{nd} (F (m))) \in V$
112	11	fvmpt2	$⊢ (m \in ℕ \land I (1^{st} (F (m))) (2^{nd} (F (m))) \in V) \to G (m) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
113	109 111 112	syl2anc	$⊢ m \in ℕ \to G (m) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
114	113	adantl	$⊢ (φ \land m \in ℕ) \to G (m) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
115	114	feq1d	$⊢ (φ \land m \in ℕ) \to (G (m) : X ⟶ ℝ^{2} \leftrightarrow I (1^{st} (F (m))) (2^{nd} (F (m))) : X ⟶ ℝ^{2})$
116	108 115	mpbird	$⊢ (φ \land m \in ℕ) \to G (m) : X ⟶ ℝ^{2}$
117	25 27 7 116	hoiprodcl2	$⊢ (φ \land m \in ℕ) \to L (G (m)) \in [0, +∞)$
118	24 117	sseldi	$⊢ (φ \land m \in ℕ) \to L (G (m)) \in [0, +∞]$
119	21 23 118	sge0xrclmpt	$⊢ φ \to sum^((m \in ℕ ⟼ L (G (m)))) \in ℝ^{*}$
120		nfv	$⊢ Ⅎ n φ$
121		0xr	$⊢ 0 \in ℝ^{*}$
122	121	a1i	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ^{*}$
123		pnfxr	$⊢ +∞ \in ℝ^{*}$
124	123	a1i	$⊢ (φ \land n \in ℕ) \to +∞ \in ℝ^{*}$
125	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
126	125 16 5	ovnval2b	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) = if (X = \emptyset, 0, sup (Z (A (n)) ℝ^{*} <))$
127	2	neneqd	$⊢ φ \to \neg X = \emptyset$
128	127	iffalsed	$⊢ φ \to if (X = \emptyset, 0, sup (Z (A (n)) ℝ^{} <)) = sup (Z (A (n)) ℝ^{} <)$
129	128	adantr	$⊢ (φ \land n \in ℕ) \to if (X = \emptyset, 0, sup (Z (A (n)) ℝ^{} <)) = sup (Z (A (n)) ℝ^{} <)$
130	126 129	eqtrd	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) = sup (Z (A (n)) ℝ^{*} <)$
131		sseq1	$⊢ a = A (n) \to (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
132	131	anbi1d	$⊢ a = A (n) \to ((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))))) \leftrightarrow (A (n) \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))))))$
133	132	rexbidv	$⊢ a = A (n) \to (\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))))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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))))))$
134	133	rabbidv	$⊢ a = A (n) \to \{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)))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\}$
135		xrex	$⊢ ℝ^{*} \in V$
136	135	rabex	$⊢ \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\} \in V$
137	136	a1i	$⊢ (φ \land n \in ℕ) \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\} \in V$
138	5 134 14 137	fvmptd3	$⊢ (φ \land n \in ℕ) \to Z (A (n)) = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\}$
139		ssrab2	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\} \subseteq ℝ^{}$
140	139	a1i	$⊢ (φ \land n \in ℕ) \to \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A (n) \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)))))\} \subseteq ℝ^{}$
141	138 140	eqsstrd	$⊢ (φ \land n \in ℕ) \to Z (A (n)) \subseteq ℝ^{*}$
142		infxrcl	$⊢ Z (A (n)) \subseteq ℝ^{} \to sup (Z (A (n)) ℝ^{} <) \in ℝ^{*}$
143	141 142	syl	$⊢ (φ \land n \in ℕ) \to sup (Z (A (n)) ℝ^{} <) \in ℝ^{}$
144	130 143	eqeltrd	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) \in ℝ^{*}$
145	4	rpred	$⊢ φ \to E \in ℝ$
146	145	adantr	$⊢ (φ \land n \in ℕ) \to E \in ℝ$
147		2re	$⊢ 2 \in ℝ$
148	147	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
149	148 78	reexpcld	$⊢ n \in ℕ \to 2^{n} \in ℝ$
150	149	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ$
151	148	recnd	$⊢ n \in ℕ \to 2 \in ℂ$
152		2ne0	$⊢ 2 \neq 0$
153	152	a1i	$⊢ n \in ℕ \to 2 \neq 0$
154		nnz	$⊢ n \in ℕ \to n \in ℤ$
155	151 153 154	expne0d	$⊢ n \in ℕ \to 2^{n} \neq 0$
156	155	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \neq 0$
157	146 150 156	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \in ℝ$
158	157	rexrd	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \in ℝ^{*}$
159	144 158	xaddcld	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \in ℝ^{*}$
160	125 16	ovncl	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) \in [0, +∞]$
161		xrge0ge0	$⊢ voln* (X) (A (n)) \in [0, +∞] \to 0 \leq voln* (X) (A (n))$
162	160 161	syl	$⊢ (φ \land n \in ℕ) \to 0 \leq voln* (X) (A (n))$
163		0red	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ$
164	82	rpgt0d	$⊢ (φ \land n \in ℕ) \to 0 < \frac{E}{2^{n}}$
165	163 157 164	ltled	$⊢ (φ \land n \in ℕ) \to 0 \leq \frac{E}{2^{n}}$
166	157	ltpnfd	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} < +∞$
167	158 124 166	xrltled	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \leq +∞$
168	122 124 158 165 167	eliccxrd	$⊢ (φ \land n \in ℕ) \to \frac{E}{2^{n}} \in [0, +∞]$
169	144 168	xadd0ge	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})$
170	122 144 159 162 169	xrletrd	$⊢ (φ \land n \in ℕ) \to 0 \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})$
171		pnfge	$⊢ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \in ℝ^{} \to voln (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \leq +∞$
172	159 171	syl	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \leq +∞$
173	122 124 159 170 172	eliccxrd	$⊢ (φ \land n \in ℕ) \to voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \in [0, +∞]$
174	120 23 173	sge0xrclmpt	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))) \in ℝ^{*}$
175		sseq1	$⊢ a = A (1^{st} (F (m))) \to (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \leftrightarrow A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k))$
176	175	rabbidv	$⊢ a = A (1^{st} (F (m))) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
177	3	adantr	$⊢ (φ \land m \in ℕ) \to A : ℕ ⟶ 𝒫 (ℝ^{X})$
178	177 34	ffvelrnd	$⊢ (φ \land m \in ℕ) \to A (1^{st} (F (m))) \in 𝒫 (ℝ^{X})$
179	52	rabex	$⊢ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \in V$
180	179	a1i	$⊢ (φ \land m \in ℕ) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \in V$
181	6 176 178 180	fvmptd3	$⊢ (φ \land m \in ℕ) \to C (A (1^{st} (F (m)))) = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
182		ssrab2	$⊢ \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
183	182	a1i	$⊢ (φ \land m \in ℕ) \to \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (1^{st} (F (m))) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
184	181 183	eqsstrd	$⊢ (φ \land m \in ℕ) \to C (A (1^{st} (F (m)))) \subseteq {({ℝ^{2}}^{X})}^{ℕ}$
185		fveq2	$⊢ a = A (1^{st} (F (m))) \to C (a) = C (A (1^{st} (F (m))))$
186	185	eleq2d	$⊢ a = A (1^{st} (F (m))) \to (i \in C (a) \leftrightarrow i \in C (A (1^{st} (F (m)))))$
187		fveq2	$⊢ a = A (1^{st} (F (m))) \to voln* (X) (a) = voln* (X) (A (1^{st} (F (m))))$
188	187	oveq1d	$⊢ a = A (1^{st} (F (m))) \to voln* (X) (a) +_{𝑒} e = voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e$
189	188	breq2d	$⊢ a = A (1^{st} (F (m))) \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e)$
190	186 189	anbi12d	$⊢ a = A (1^{st} (F (m))) \to ((i \in C (a) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e) \leftrightarrow (i \in C (A (1^{st} (F (m)))) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e))$
191	190	rabbidva2	$⊢ a = A (1^{st} (F (m))) \to \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\} = \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\}$
192	191	mpteq2dv	$⊢ a = A (1^{st} (F (m))) \to (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}) = (e \in ℝ^{+} ⟼ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\})$
193	67	mptex	$⊢ (e \in ℝ^{+} ⟼ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\}) \in V$
194	193	a1i	$⊢ (φ \land m \in ℕ) \to (e \in ℝ^{+} ⟼ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\}) \in V$
195	8 192 178 194	fvmptd3	$⊢ (φ \land m \in ℕ) \to D (A (1^{st} (F (m)))) = (e \in ℝ^{+} ⟼ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\})$
196		oveq2	$⊢ e = \frac{E}{2^{1^{st} (F (m))}} \to voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e = voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})$
197	196	breq2d	$⊢ e = \frac{E}{2^{1^{st} (F (m))}} \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}}))$
198	197	rabbidv	$⊢ e = \frac{E}{2^{1^{st} (F (m))}} \to \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\} = \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\}$
199	198	adantl	$⊢ ((φ \land m \in ℕ) \land e = \frac{E}{2^{1^{st} (F (m))}}) \to \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} e\} = \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\}$
200	26 4	syl	$⊢ (φ \land m \in ℕ) \to E \in ℝ^{+}$
201		2rp	$⊢ 2 \in ℝ^{+}$
202	201	a1i	$⊢ (φ \land m \in ℕ) \to 2 \in ℝ^{+}$
203	34	nnzd	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) \in ℤ$
204	202 203	rpexpcld	$⊢ (φ \land m \in ℕ) \to 2^{1^{st} (F (m))} \in ℝ^{+}$
205	200 204	rpdivcld	$⊢ (φ \land m \in ℕ) \to \frac{E}{2^{1^{st} (F (m))}} \in ℝ^{+}$
206		fvex	$⊢ C (A (1^{st} (F (m)))) \in V$
207	206	rabex	$⊢ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\} \in V$
208	207	a1i	$⊢ (φ \land m \in ℕ) \to \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\} \in V$
209	195 199 205 208	fvmptd	$⊢ (φ \land m \in ℕ) \to D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}}) = \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\}$
210		ssrab2	$⊢ \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\} \subseteq C (A (1^{st} (F (m))))$
211	210	a1i	$⊢ (φ \land m \in ℕ) \to \{i \in C (A (1^{st} (F (m)))) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (1^{st} (F (m)))) +_{𝑒} (\frac{E}{2^{1^{st} (F (m))}})\} \subseteq C (A (1^{st} (F (m))))$
212	209 211	eqsstrd	$⊢ (φ \land m \in ℕ) \to D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}}) \subseteq C (A (1^{st} (F (m))))$
213	44	anbi2d	$⊢ n = 1^{st} (F (m)) \to ((φ \land n \in ℕ) \leftrightarrow (φ \land 1^{st} (F (m)) \in ℕ))$
214		2fveq3	$⊢ n = 1^{st} (F (m)) \to D (A (n)) = D (A (1^{st} (F (m))))$
215		oveq2	$⊢ n = 1^{st} (F (m)) \to 2^{n} = 2^{1^{st} (F (m))}$
216	215	oveq2d	$⊢ n = 1^{st} (F (m)) \to \frac{E}{2^{n}} = \frac{E}{2^{1^{st} (F (m))}}$
217	214 216	fveq12d	$⊢ n = 1^{st} (F (m)) \to D (A (n)) (\frac{E}{2^{n}}) = D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}})$
218	46 217	eleq12d	$⊢ n = 1^{st} (F (m)) \to (I (n) \in D (A (n)) (\frac{E}{2^{n}}) \leftrightarrow I (1^{st} (F (m))) \in D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}}))$
219	213 218	imbi12d	$⊢ n = 1^{st} (F (m)) \to (((φ \land n \in ℕ) \to I (n) \in D (A (n)) (\frac{E}{2^{n}})) \leftrightarrow ((φ \land 1^{st} (F (m)) \in ℕ) \to I (1^{st} (F (m))) \in D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}})))$
220	43 219 9	vtocl	$⊢ (φ \land 1^{st} (F (m)) \in ℕ) \to I (1^{st} (F (m))) \in D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}})$
221	26 34 220	syl2anc	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) \in D (A (1^{st} (F (m)))) (\frac{E}{2^{1^{st} (F (m))}})$
222	212 221	sseldd	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) \in C (A (1^{st} (F (m))))$
223	184 222	sseldd	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) \in ({({ℝ^{2}}^{X})}^{ℕ})$
224		elmapfn	$⊢ I (1^{st} (F (m))) \in ({({ℝ^{2}}^{X})}^{ℕ}) \to I (1^{st} (F (m))) Fn ℕ$
225	223 224	syl	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) Fn ℕ$
226		elmapi	$⊢ I (1^{st} (F (m))) \in ({({ℝ^{2}}^{X})}^{ℕ}) \to I (1^{st} (F (m))) : ℕ ⟶ {ℝ^{2}}^{X}$
227	223 226	syl	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) : ℕ ⟶ {ℝ^{2}}^{X}$
228	227	ffvelrnda	$⊢ ((φ \land m \in ℕ) \land j \in ℕ) \to I (1^{st} (F (m))) (j) \in ({ℝ^{2}}^{X})$
229	228	ralrimiva	$⊢ (φ \land m \in ℕ) \to \forall j \in ℕ I (1^{st} (F (m))) (j) \in ({ℝ^{2}}^{X})$
230	225 229	jca	$⊢ (φ \land m \in ℕ) \to (I (1^{st} (F (m))) Fn ℕ \land \forall j \in ℕ I (1^{st} (F (m))) (j) \in ({ℝ^{2}}^{X}))$
231		ffnfv	$⊢ I (1^{st} (F (m))) : ℕ ⟶ {ℝ^{2}}^{X} \leftrightarrow (I (1^{st} (F (m))) Fn ℕ \land \forall j \in ℕ I (1^{st} (F (m))) (j) \in ({ℝ^{2}}^{X}))$
232	230 231	sylibr	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) : ℕ ⟶ {ℝ^{2}}^{X}$
233	232 36	ffvelrnd	$⊢ (φ \land m \in ℕ) \to I (1^{st} (F (m))) (2^{nd} (F (m))) \in ({ℝ^{2}}^{X})$
234	233 11	fmptd	$⊢ φ \to G : ℕ ⟶ {ℝ^{2}}^{X}$
235		simpl	$⊢ (φ \land n \in ℕ) \to φ$
236	9 86	eleqtrd	$⊢ (φ \land n \in ℕ) \to I (n) \in \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\}$
237	87 236	sseldi	$⊢ (φ \land n \in ℕ) \to I (n) \in C (A (n))$
238		simp3	$⊢ (φ \land n \in ℕ \land I (n) \in C (A (n))) \to I (n) \in C (A (n))$
239	55	3adant3	$⊢ (φ \land n \in ℕ \land I (n) \in C (A (n))) \to C (A (n)) = \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
240	238 239	eleqtrd	$⊢ (φ \land n \in ℕ \land I (n) \in C (A (n))) \to I (n) \in \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\}$
241		fveq1	$⊢ h = I (n) \to h (j) = I (n) (j)$
242	241	coeq2d	$⊢ h = I (n) \to [.) \circ h (j) = [.) \circ I (n) (j)$
243	242	fveq1d	$⊢ h = I (n) \to ([.) \circ h (j)) (k) = ([.) \circ I (n) (j)) (k)$
244	243	ixpeq2dv	$⊢ h = I (n) \to \underset{k \in X}{⨉} ([.) \circ h (j)) (k) = \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k)$
245	244	iuneq2d	$⊢ h = I (n) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k)$
246	245	sseq2d	$⊢ h = I (n) \to (A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \leftrightarrow A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k))$
247	246	elrab	$⊢ I (n) \in \{h \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k)\} \leftrightarrow (I (n) \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k))$
248	240 247	sylib	$⊢ (φ \land n \in ℕ \land I (n) \in C (A (n))) \to (I (n) \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k))$
249	248	simprd	$⊢ (φ \land n \in ℕ \land I (n) \in C (A (n))) \to A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k)$
250	235 13 237 249	syl3anc	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k)$
251		f1ofo	$⊢ F : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to F : ℕ \underset{onto}{⟶} ℕ \times ℕ$
252	10 251	syl	$⊢ φ \to F : ℕ \underset{onto}{⟶} ℕ \times ℕ$
253	252	ad2antrr	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to F : ℕ \underset{onto}{⟶} ℕ \times ℕ$
254		opelxpi	$⊢ (n \in ℕ \land j \in ℕ) \to ⟨n, j⟩ \in (ℕ \times ℕ)$
255	13 254	sylan	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to ⟨n, j⟩ \in (ℕ \times ℕ)$
256		foelrni	$⊢ (F : ℕ \underset{onto}{⟶} ℕ \times ℕ \land ⟨n, j⟩ \in (ℕ \times ℕ)) \to \exists m \in ℕ F (m) = ⟨n, j⟩$
257	253 255 256	syl2anc	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to \exists m \in ℕ F (m) = ⟨n, j⟩$
258		nfv	$⊢ Ⅎ m ((φ \land n \in ℕ) \land j \in ℕ)$
259		nfre1	$⊢ Ⅎ m \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
260		simpl	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to m \in ℕ$
261		fveq2	$⊢ F (m) = ⟨n, j⟩ \to 1^{st} (F (m)) = 1^{st} (⟨n, j⟩)$
262		op1stg	$⊢ (n \in V \land j \in V) \to 1^{st} (⟨n, j⟩) = n$
263	262	el2v	$⊢ 1^{st} (⟨n, j⟩) = n$
264	263	a1i	$⊢ F (m) = ⟨n, j⟩ \to 1^{st} (⟨n, j⟩) = n$
265	261 264	eqtrd	$⊢ F (m) = ⟨n, j⟩ \to 1^{st} (F (m)) = n$
266	265	adantl	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to 1^{st} (F (m)) = n$
267	260 266	jca	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to (m \in ℕ \land 1^{st} (F (m)) = n)$
268		2fveq3	$⊢ i = m \to 1^{st} (F (i)) = 1^{st} (F (m))$
269	268	eqeq1d	$⊢ i = m \to (1^{st} (F (i)) = n \leftrightarrow 1^{st} (F (m)) = n)$
270	269	elrab	$⊢ m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \leftrightarrow (m \in ℕ \land 1^{st} (F (m)) = n)$
271	267 270	sylibr	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}$
272	271	3adant1	$⊢ (((φ \land n \in ℕ) \land j \in ℕ) \land m \in ℕ \land F (m) = ⟨n, j⟩) \to m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}$
273	260 113	syl	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to G (m) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
274	265	fveq2d	$⊢ F (m) = ⟨n, j⟩ \to I (1^{st} (F (m))) = I (n)$
275		vex	$⊢ n \in V$
276		vex	$⊢ j \in V$
277	275 276	op2ndd	$⊢ F (m) = ⟨n, j⟩ \to 2^{nd} (F (m)) = j$
278	274 277	fveq12d	$⊢ F (m) = ⟨n, j⟩ \to I (1^{st} (F (m))) (2^{nd} (F (m))) = I (n) (j)$
279	278	adantl	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to I (1^{st} (F (m))) (2^{nd} (F (m))) = I (n) (j)$
280	273 279	eqtr2d	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to I (n) (j) = G (m)$
281	280	coeq2d	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to [.) \circ I (n) (j) = [.) \circ G (m)$
282	281	fveq1d	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to ([.) \circ I (n) (j)) (k) = ([.) \circ G (m)) (k)$
283	282	ixpeq2dv	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) = \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
284		eqimss	$⊢ \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) = \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \to \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
285	283 284	syl	$⊢ (m \in ℕ \land F (m) = ⟨n, j⟩) \to \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
286	285	3adant1	$⊢ (((φ \land n \in ℕ) \land j \in ℕ) \land m \in ℕ \land F (m) = ⟨n, j⟩) \to \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
287		rspe	$⊢ (m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \land \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)) \to \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
288	272 286 287	syl2anc	$⊢ (((φ \land n \in ℕ) \land j \in ℕ) \land m \in ℕ \land F (m) = ⟨n, j⟩) \to \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
289	288	3exp	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to (m \in ℕ \to (F (m) = ⟨n, j⟩ \to \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)))$
290	258 259 289	rexlimd	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to (\exists m \in ℕ F (m) = ⟨n, j⟩ \to \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k))$
291	257 290	mpd	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
292	291	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall j \in ℕ \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
293		iunss2	$⊢ \forall j \in ℕ \exists m \in \{i \in ℕ \| 1^{st} (F (i)) = n\} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
294	292 293	syl	$⊢ (φ \land n \in ℕ) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ I (n) (j)) (k) \subseteq ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
295	250 294	sstrd	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
296		ssrab2	$⊢ \{i \in ℕ \| 1^{st} (F (i)) = n\} \subseteq ℕ$
297		iunss1	$⊢ \{i \in ℕ \| 1^{st} (F (i)) = n\} \subseteq ℕ \to ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
298	296 297	ax-mp	$⊢ ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
299	298	a1i	$⊢ (φ \land n \in ℕ) \to ⋃_{m \in \{i \in ℕ \| 1^{st} (F (i)) = n\}} \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
300	295 299	sstrd	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
301	300	ralrimiva	$⊢ φ \to \forall n \in ℕ A (n) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
302		iunss	$⊢ ⋃_{n \in ℕ} A (n) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k) \leftrightarrow \forall n \in ℕ A (n) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
303	301 302	sylibr	$⊢ φ \to ⋃_{n \in ℕ} A (n) \subseteq ⋃_{m \in ℕ} \underset{k \in X}{⨉} ([.) \circ G (m)) (k)$
304	1 2 7 234 303	ovnlecvr	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((m \in ℕ ⟼ L (G (m))))$
305	114	fveq2d	$⊢ (φ \land m \in ℕ) \to L (G (m)) = L (I (1^{st} (F (m))) (2^{nd} (F (m))))$
306	305	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ L (G (m))) = (m \in ℕ ⟼ L (I (1^{st} (F (m))) (2^{nd} (F (m)))))$
307	306	fveq2d	$⊢ φ \to sum^((m \in ℕ ⟼ L (G (m)))) = sum^((m \in ℕ ⟼ L (I (1^{st} (F (m))) (2^{nd} (F (m))))))$
308		nfv	$⊢ Ⅎ p φ$
309		2fveq3	$⊢ p = F (m) \to I (1^{st} (p)) = I (1^{st} (F (m)))$
310		fveq2	$⊢ p = F (m) \to 2^{nd} (p) = 2^{nd} (F (m))$
311	309 310	fveq12d	$⊢ p = F (m) \to I (1^{st} (p)) (2^{nd} (p)) = I (1^{st} (F (m))) (2^{nd} (F (m)))$
312	311	fveq2d	$⊢ p = F (m) \to L (I (1^{st} (p)) (2^{nd} (p))) = L (I (1^{st} (F (m))) (2^{nd} (F (m))))$
313		eqidd	$⊢ (φ \land m \in ℕ) \to F (m) = F (m)$
314		nfv	$⊢ Ⅎ k (φ \land p \in (ℕ \times ℕ))$
315	1	adantr	$⊢ (φ \land p \in (ℕ \times ℕ)) \to X \in Fin$
316		simpl	$⊢ (φ \land p \in (ℕ \times ℕ)) \to φ$
317		xp1st	$⊢ p \in (ℕ \times ℕ) \to 1^{st} (p) \in ℕ$
318	317	adantl	$⊢ (φ \land p \in (ℕ \times ℕ)) \to 1^{st} (p) \in ℕ$
319		xp2nd	$⊢ p \in (ℕ \times ℕ) \to 2^{nd} (p) \in ℕ$
320	319	adantl	$⊢ (φ \land p \in (ℕ \times ℕ)) \to 2^{nd} (p) \in ℕ$
321		fvex	$⊢ 2^{nd} (p) \in V$
322		eleq1	$⊢ j = 2^{nd} (p) \to (j \in ℕ \leftrightarrow 2^{nd} (p) \in ℕ)$
323	322	3anbi3d	$⊢ j = 2^{nd} (p) \to ((φ \land 1^{st} (p) \in ℕ \land j \in ℕ) \leftrightarrow (φ \land 1^{st} (p) \in ℕ \land 2^{nd} (p) \in ℕ))$
324		fveq2	$⊢ j = 2^{nd} (p) \to I (1^{st} (p)) (j) = I (1^{st} (p)) (2^{nd} (p))$
325	324	feq1d	$⊢ j = 2^{nd} (p) \to (I (1^{st} (p)) (j) : X ⟶ ℝ^{2} \leftrightarrow I (1^{st} (p)) (2^{nd} (p)) : X ⟶ ℝ^{2})$
326	323 325	imbi12d	$⊢ j = 2^{nd} (p) \to (((φ \land 1^{st} (p) \in ℕ \land j \in ℕ) \to I (1^{st} (p)) (j) : X ⟶ ℝ^{2}) \leftrightarrow ((φ \land 1^{st} (p) \in ℕ \land 2^{nd} (p) \in ℕ) \to I (1^{st} (p)) (2^{nd} (p)) : X ⟶ ℝ^{2}))$
327		fvex	$⊢ 1^{st} (p) \in V$
328		eleq1	$⊢ n = 1^{st} (p) \to (n \in ℕ \leftrightarrow 1^{st} (p) \in ℕ)$
329	328	3anbi2d	$⊢ n = 1^{st} (p) \to ((φ \land n \in ℕ \land j \in ℕ) \leftrightarrow (φ \land 1^{st} (p) \in ℕ \land j \in ℕ))$
330		fveq2	$⊢ n = 1^{st} (p) \to I (n) = I (1^{st} (p))$
331	330	fveq1d	$⊢ n = 1^{st} (p) \to I (n) (j) = I (1^{st} (p)) (j)$
332	331	feq1d	$⊢ n = 1^{st} (p) \to (I (n) (j) : X ⟶ ℝ^{2} \leftrightarrow I (1^{st} (p)) (j) : X ⟶ ℝ^{2})$
333	329 332	imbi12d	$⊢ n = 1^{st} (p) \to (((φ \land n \in ℕ \land j \in ℕ) \to I (n) (j) : X ⟶ ℝ^{2}) \leftrightarrow ((φ \land 1^{st} (p) \in ℕ \land j \in ℕ) \to I (1^{st} (p)) (j) : X ⟶ ℝ^{2}))$
334	327 333 105	vtocl	$⊢ (φ \land 1^{st} (p) \in ℕ \land j \in ℕ) \to I (1^{st} (p)) (j) : X ⟶ ℝ^{2}$
335	321 326 334	vtocl	$⊢ (φ \land 1^{st} (p) \in ℕ \land 2^{nd} (p) \in ℕ) \to I (1^{st} (p)) (2^{nd} (p)) : X ⟶ ℝ^{2}$
336	316 318 320 335	syl3anc	$⊢ (φ \land p \in (ℕ \times ℕ)) \to I (1^{st} (p)) (2^{nd} (p)) : X ⟶ ℝ^{2}$
337	314 315 7 336	hoiprodcl2	$⊢ (φ \land p \in (ℕ \times ℕ)) \to L (I (1^{st} (p)) (2^{nd} (p))) \in [0, +∞)$
338	24 337	sseldi	$⊢ (φ \land p \in (ℕ \times ℕ)) \to L (I (1^{st} (p)) (2^{nd} (p))) \in [0, +∞]$
339	308 21 312 23 10 313 338	sge0f1o	$⊢ φ \to sum^((p \in (ℕ \times ℕ) ⟼ L (I (1^{st} (p)) (2^{nd} (p))))) = sum^((m \in ℕ ⟼ L (I (1^{st} (F (m))) (2^{nd} (F (m))))))$
340	307 339	eqtr4d	$⊢ φ \to sum^((m \in ℕ ⟼ L (G (m)))) = sum^((p \in (ℕ \times ℕ) ⟼ L (I (1^{st} (p)) (2^{nd} (p)))))$
341		nfv	$⊢ Ⅎ j φ$
342	275 276	op1std	$⊢ p = ⟨n, j⟩ \to 1^{st} (p) = n$
343	342	fveq2d	$⊢ p = ⟨n, j⟩ \to I (1^{st} (p)) = I (n)$
344	275 276	op2ndd	$⊢ p = ⟨n, j⟩ \to 2^{nd} (p) = j$
345	343 344	fveq12d	$⊢ p = ⟨n, j⟩ \to I (1^{st} (p)) (2^{nd} (p)) = I (n) (j)$
346	345	fveq2d	$⊢ p = ⟨n, j⟩ \to L (I (1^{st} (p)) (2^{nd} (p))) = L (I (n) (j))$
347		nfv	$⊢ Ⅎ k ((φ \land n \in ℕ) \land j \in ℕ)$
348	125	adantr	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to X \in Fin$
349	96 104	syl	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to I (n) (j) : X ⟶ ℝ^{2}$
350	347 348 7 349	hoiprodcl2	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to L (I (n) (j)) \in [0, +∞)$
351	24 350	sseldi	$⊢ ((φ \land n \in ℕ) \land j \in ℕ) \to L (I (n) (j)) \in [0, +∞]$
352	351	3impa	$⊢ (φ \land n \in ℕ \land j \in ℕ) \to L (I (n) (j)) \in [0, +∞]$
353	341 346 23 23 352	sge0xp	$⊢ φ \to sum^((n \in ℕ ⟼ sum^((j \in ℕ ⟼ L (I (n) (j)))))) = sum^((p \in (ℕ \times ℕ) ⟼ L (I (1^{st} (p)) (2^{nd} (p)))))$
354	353	eqcomd	$⊢ φ \to sum^((p \in (ℕ \times ℕ) ⟼ L (I (1^{st} (p)) (2^{nd} (p))))) = sum^((n \in ℕ ⟼ sum^((j \in ℕ ⟼ L (I (n) (j))))))$
355	22	a1i	$⊢ (φ \land n \in ℕ) \to ℕ \in V$
356		eqid	$⊢ (j \in ℕ ⟼ L (I (n) (j))) = (j \in ℕ ⟼ L (I (n) (j)))$
357	351 356	fmptd	$⊢ (φ \land n \in ℕ) \to (j \in ℕ ⟼ L (I (n) (j))) : ℕ ⟶ [0, +∞]$
358	355 357	sge0cl	$⊢ (φ \land n \in ℕ) \to sum^((j \in ℕ ⟼ L (I (n) (j)))) \in [0, +∞]$
359		fveq1	$⊢ i = I (n) \to i (j) = I (n) (j)$
360	359	fveq2d	$⊢ i = I (n) \to L (i (j)) = L (I (n) (j))$
361	360	mpteq2dv	$⊢ i = I (n) \to (j \in ℕ ⟼ L (i (j))) = (j \in ℕ ⟼ L (I (n) (j)))$
362	361	fveq2d	$⊢ i = I (n) \to sum^((j \in ℕ ⟼ L (i (j)))) = sum^((j \in ℕ ⟼ L (I (n) (j))))$
363	362	breq1d	$⊢ i = I (n) \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}) \leftrightarrow sum^((j \in ℕ ⟼ L (I (n) (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))$
364	363	elrab	$⊢ I (n) \in \{i \in C (A (n)) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})\} \leftrightarrow (I (n) \in C (A (n)) \land sum^((j \in ℕ ⟼ L (I (n) (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))$
365	236 364	sylib	$⊢ (φ \land n \in ℕ) \to (I (n) \in C (A (n)) \land sum^((j \in ℕ ⟼ L (I (n) (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))$
366	365	simprd	$⊢ (φ \land n \in ℕ) \to sum^((j \in ℕ ⟼ L (I (n) (j)))) \leq voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})$
367	120 23 358 173 366	sge0lempt	$⊢ φ \to sum^((n \in ℕ ⟼ sum^((j \in ℕ ⟼ L (I (n) (j)))))) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})))$
368	354 367	eqbrtrd	$⊢ φ \to sum^((p \in (ℕ \times ℕ) ⟼ L (I (1^{st} (p)) (2^{nd} (p))))) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})))$
369	340 368	eqbrtrd	$⊢ φ \to sum^((m \in ℕ ⟼ L (G (m)))) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})))$
370	20 119 174 304 369	xrletrd	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}})))$
371	120 23 160 168	sge0xadd	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))) = sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} sum^((n \in ℕ ⟼ \frac{E}{2^{n}}))$
372	121	a1i	$⊢ φ \to 0 \in ℝ^{*}$
373	123	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
374	145	rexrd	$⊢ φ \to E \in ℝ^{*}$
375	4	rpge0d	$⊢ φ \to 0 \leq E$
376	145	ltpnfd	$⊢ φ \to E < +∞$
377	372 373 374 375 376	elicod	$⊢ φ \to E \in [0, +∞)$
378	377	sge0ad2en	$⊢ φ \to sum^((n \in ℕ ⟼ \frac{E}{2^{n}})) = E$
379	378	oveq2d	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} sum^((n \in ℕ ⟼ \frac{E}{2^{n}})) = sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
380	371 379	eqtrd	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (A (n)) +_{𝑒} (\frac{E}{2^{n}}))) = sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$
381	370 380	breqtrd	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (A (n)))) +_{𝑒} E$

Metamath Proof Explorer

Theorem ovnsubaddlem1

Proof