ovncvrrp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ovncvrrp.x	$⊢ φ \to X \in Fin$
2		ovncvrrp.n0	$⊢ φ \to X \neq \emptyset$
3		ovncvrrp.a	$⊢ φ \to A \subseteq ℝ^{X}$
4		ovncvrrp.e	$⊢ φ \to E \in ℝ^{+}$
5		ovncvrrp.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
6		ovncvrrp.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
7		ovncvrrp.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}))$
8		eqid	$⊢ \{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 \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)))))\}$
9	1 2 3 4 8	ovnlerp	$⊢ φ \to \exists z \in \{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 \leq voln (X) (A) +_{𝑒} E$
10		simp1	$⊢ (φ \land z \in \{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)))))\} \land z \leq voln (X) (A) +_{𝑒} E) \to φ$
11		simp3	$⊢ (φ \land z \in \{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)))))\} \land z \leq voln (X) (A) +_{𝑒} E) \to z \leq voln* (X) (A) +_{𝑒} E$
12		rabid	$⊢ z \in \{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)))))\} \leftrightarrow (z \in ℝ^{} \land \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))))))$
13	12	biimpi	$⊢ z \in \{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)))))\} \to (z \in ℝ^{} \land \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))))))$
14	13	simprd	$⊢ z \in \{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)))))\} \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)))))$
15	14	adantr	$⊢ (z \in \{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)))))\} \land z \leq voln (X) (A) +_{𝑒} E) \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)))))$
16	15	3adant1	$⊢ (φ \land z \in \{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)))))\} \land z \leq voln (X) (A) +_{𝑒} E) \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)))))$
17		nfv	$⊢ Ⅎ i (φ \land z \leq voln* (X) (A) +_{𝑒} E)$
18		nfe1	$⊢ Ⅎ i \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
19		simp1l	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to φ$
20		simp2	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to i \in ({({ℝ^{2}}^{X})}^{ℕ})$
21		simp3l	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
22		id	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
23		fveq1	$⊢ l = i \to l (j) = i (j)$
24	23	coeq2d	$⊢ l = i \to [.) \circ l (j) = [.) \circ i (j)$
25	24	fveq1d	$⊢ l = i \to ([.) \circ l (j)) (k) = ([.) \circ i (j)) (k)$
26	25	ixpeq2dv	$⊢ l = i \to \underset{k \in X}{⨉} ([.) \circ l (j)) (k) = \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
27	26	iuneq2d	$⊢ l = i \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
28	27	sseq2d	$⊢ l = i \to (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
29	28	elrab	$⊢ i \in \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \leftrightarrow (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
30	22 29	sylibr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to i \in \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
31	30	3adant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to i \in \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
32		sseq1	$⊢ a = A \to (a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k))$
33	32	rabbidv	$⊢ a = A \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \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)\}$
34		ovexd	$⊢ φ \to ℝ^{X} \in V$
35	34 3	ssexd	$⊢ φ \to A \in V$
36		elpwg	$⊢ A \in V \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
37	35 36	syl	$⊢ φ \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
38	3 37	mpbird	$⊢ φ \to A \in 𝒫 (ℝ^{X})$
39		ovex	$⊢ {({ℝ^{2}}^{X})}^{ℕ} \in V$
40	39	rabex	$⊢ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \in V$
41	40	a1i	$⊢ φ \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} \in V$
42	5 33 38 41	fvmptd3	$⊢ φ \to C (A) = \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\}$
43	42	eqcomd	$⊢ φ \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} = C (A)$
44	43	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\} = C (A)$
45	31 44	eleqtrd	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to i \in C (A)$
46	19 20 21 45	syl3anc	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to i \in C (A)$
47		coeq2	$⊢ h = i (j) \to [.) \circ h = [.) \circ i (j)$
48	47	fveq1d	$⊢ h = i (j) \to ([.) \circ h) (k) = ([.) \circ i (j)) (k)$
49	48	fveq2d	$⊢ h = i (j) \to vol (([.) \circ h) (k)) = vol (([.) \circ i (j)) (k))$
50	49	prodeq2ad	$⊢ h = i (j) \to \prod_{k \in X} vol (([.) \circ h) (k)) = \prod_{k \in X} vol (([.) \circ i (j)) (k))$
51		elmapi	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to i : ℕ ⟶ {ℝ^{2}}^{X}$
52	51	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to i : ℕ ⟶ {ℝ^{2}}^{X}$
53		simpr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to j \in ℕ$
54	52 53	ffvelcdmd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to i (j) \in ({ℝ^{2}}^{X})$
55		prodex	$⊢ \prod_{k \in X} vol (([.) \circ i (j)) (k)) \in V$
56	55	a1i	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to \prod_{k \in X} vol (([.) \circ i (j)) (k)) \in V$
57	6 50 54 56	fvmptd3	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to L (i (j)) = \prod_{k \in X} vol (([.) \circ i (j)) (k))$
58	57	mpteq2dva	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (j \in ℕ ⟼ L (i (j))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
59	58	fveq2d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to sum^((j \in ℕ ⟼ L (i (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
60	59	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ L (i (j)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
61		id	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \to z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
62	61	eqcomd	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) = z$
63	62	adantl	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) = z$
64	60 63	eqtrd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ L (i (j)))) = z$
65	64	3adant1	$⊢ (z \leq voln* (X) (A) +_{𝑒} E \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ L (i (j)))) = z$
66		simp1	$⊢ (z \leq voln* (X) (A) +_{𝑒} E \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z \leq voln* (X) (A) +_{𝑒} E$
67	65 66	eqbrtrd	$⊢ (z \leq voln* (X) (A) +_{𝑒} E \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E$
68	67	3adant1l	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E$
69	68	3adant3l	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E$
70	46 69	jca	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
71	70	19.8ad	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (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)))))) \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
72	71	3exp	$⊢ (φ \land z \leq voln* (X) (A) +_{𝑒} E) \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \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))))) \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)))$
73	17 18 72	rexlimd	$⊢ (φ \land z \leq voln* (X) (A) +_{𝑒} E) \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))))) \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E))$
74	73	imp	$⊢ ((φ \land z \leq voln* (X) (A) +_{𝑒} E) \land \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)))))) \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
75	10 11 16 74	syl21anc	$⊢ (φ \land z \in \{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)))))\} \land z \leq voln (X) (A) +_{𝑒} E) \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
76	75	3exp	$⊢ φ \to (z \in \{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)))))\} \to (z \leq voln (X) (A) +_{𝑒} E \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)))$
77	76	rexlimdv	$⊢ φ \to (\exists z \in \{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 \leq voln (X) (A) +_{𝑒} E \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E))$
78	9 77	mpd	$⊢ φ \to \exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
79		rabid	$⊢ i \in \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \leftrightarrow (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
80	79	bilanri	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to i \in \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
81		nfcv	$⊢ \underline{Ⅎ} b (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\})$
82		nfcv	$⊢ \underline{Ⅎ} a ℝ^{+}$
83		nfv	$⊢ Ⅎ a sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e$
84		nfmpt1	$⊢ \underline{Ⅎ} a (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
85	5 84	nfcxfr	$⊢ \underline{Ⅎ} a C$
86		nfcv	$⊢ \underline{Ⅎ} a b$
87	85 86	nffv	$⊢ \underline{Ⅎ} a C (b)$
88	83 87	nfrabw	$⊢ \underline{Ⅎ} a \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\}$
89	82 88	nfmpt	$⊢ \underline{Ⅎ} a (e \in ℝ^{+} ⟼ \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\})$
90		fveq2	$⊢ a = b \to C (a) = C (b)$
91	90	eleq2d	$⊢ a = b \to (i \in C (a) \leftrightarrow i \in C (b))$
92		fveq2	$⊢ a = b \to voln* (X) (a) = voln* (X) (b)$
93	92	oveq1d	$⊢ a = b \to voln* (X) (a) +_{𝑒} e = voln* (X) (b) +_{𝑒} e$
94	93	breq2d	$⊢ a = b \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e)$
95	91 94	anbi12d	$⊢ a = b \to ((i \in C (a) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e) \leftrightarrow (i \in C (b) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e))$
96	95	rabbidva2	$⊢ a = b \to \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\} = \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\}$
97	96	mpteq2dv	$⊢ a = b \to (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\}) = (e \in ℝ^{+} ⟼ \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\})$
98	81 89 97	cbvmpt	$⊢ (a \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} e\})) = (b \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\}))$
99	7 98	eqtri	$⊢ D = (b \in 𝒫 (ℝ^{X}) ⟼ (e \in ℝ^{+} ⟼ \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\}))$
100		fveq2	$⊢ b = A \to C (b) = C (A)$
101	100	eleq2d	$⊢ b = A \to (i \in C (b) \leftrightarrow i \in C (A))$
102		fveq2	$⊢ b = A \to voln* (X) (b) = voln* (X) (A)$
103	102	oveq1d	$⊢ b = A \to voln* (X) (b) +_{𝑒} e = voln* (X) (A) +_{𝑒} e$
104	103	breq2d	$⊢ b = A \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e)$
105	101 104	anbi12d	$⊢ b = A \to ((i \in C (b) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e) \leftrightarrow (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e))$
106	105	rabbidva2	$⊢ b = A \to \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\}$
107	106	mpteq2dv	$⊢ b = A \to (e \in ℝ^{+} ⟼ \{i \in C (b) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (b) +_{𝑒} e\}) = (e \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\})$
108	38	adantr	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to A \in 𝒫 (ℝ^{X})$
109		rpex	$⊢ ℝ^{+} \in V$
110	109	mptex	$⊢ (e \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\}) \in V$
111	110	a1i	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to (e \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\}) \in V$
112	99 107 108 111	fvmptd3	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to D (A) = (e \in ℝ^{+} ⟼ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\})$
113		oveq2	$⊢ e = E \to voln* (X) (A) +_{𝑒} e = voln* (X) (A) +_{𝑒} E$
114	113	breq2d	$⊢ e = E \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e \leftrightarrow sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)$
115	114	rabbidv	$⊢ e = E \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
116	115	adantl	$⊢ ((φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \land e = E) \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} e\} = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
117	4	adantr	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to E \in ℝ^{+}$
118		fvex	$⊢ C (A) \in V$
119	118	rabex	$⊢ \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \in V$
120	119	a1i	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} \in V$
121	112 116 117 120	fvmptd	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to D (A) (E) = \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\}$
122	121	eqcomd	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to \{i \in C (A) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E\} = D (A) (E)$
123	80 122	eleqtrd	$⊢ (φ \land (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E)) \to i \in D (A) (E)$
124	123	ex	$⊢ φ \to ((i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E) \to i \in D (A) (E))$
125	124	eximdv	$⊢ φ \to (\exists i (i \in C (A) \land sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (A) +_{𝑒} E) \to \exists i i \in D (A) (E))$
126	78 125	mpd	$⊢ φ \to \exists i i \in D (A) (E)$

Metamath Proof Explorer

Theorem ovncvrrp

Proof