ovnhoilem2

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	ovnhoilem2.x	$⊢ φ \to X \in Fin$
	ovnhoilem2.n	$⊢ φ \to X \neq \emptyset$
	ovnhoilem2.a	$⊢ φ \to A : X ⟶ ℝ$
	ovnhoilem2.b	$⊢ φ \to B : X ⟶ ℝ$
	ovnhoilem2.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
	ovnhoilem2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	ovnhoilem2.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
	ovnhoilem2.f	$⊢ F = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))))$
	ovnhoilem2.s	$⊢ S = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))))$
Assertion	ovnhoilem2	$⊢ φ \to A L (X) B \leq voln* (X) (I)$

Proof

Step	Hyp	Ref	Expression
1		ovnhoilem2.x	$⊢ φ \to X \in Fin$
2		ovnhoilem2.n	$⊢ φ \to X \neq \emptyset$
3		ovnhoilem2.a	$⊢ φ \to A : X ⟶ ℝ$
4		ovnhoilem2.b	$⊢ φ \to B : X ⟶ ℝ$
5		ovnhoilem2.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
6		ovnhoilem2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
7		ovnhoilem2.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
8		ovnhoilem2.f	$⊢ F = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))))$
9		ovnhoilem2.s	$⊢ S = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))))$
10	7	eleq2i	$⊢ z \in M \leftrightarrow z \in \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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)))))\}$
11		rabid	$⊢ z \in \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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})}^{ℕ}) (I \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))))))$
12	10 11	bitri	$⊢ z \in M \leftrightarrow (z \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 M \to (z \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 M \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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	adantl	$⊢ (φ \land z \in M) \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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	1	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 X \in Fin$
17	3	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 : X ⟶ ℝ$
18	4	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 B : X ⟶ ℝ$
19		elmapi	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to i : ℕ ⟶ {ℝ^{2}}^{X}$
20	19	ffvelrnda	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to i (n) \in ({ℝ^{2}}^{X})$
21		elmapi	$⊢ i (n) \in ({ℝ^{2}}^{X}) \to i (n) : X ⟶ ℝ^{2}$
22	20 21	syl	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to i (n) : X ⟶ ℝ^{2}$
23	22	ffvelrnda	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land l \in X) \to i (n) (l) \in ℝ^{2}$
24		xp1st	$⊢ i (n) (l) \in ℝ^{2} \to 1^{st} (i (n) (l)) \in ℝ$
25	23 24	syl	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land l \in X) \to 1^{st} (i (n) (l)) \in ℝ$
26	25	fmpttd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 1^{st} (i (n) (l))) : X ⟶ ℝ$
27		reex	$⊢ ℝ \in V$
28	27	a1i	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to ℝ \in V$
29		1nn	$⊢ 1 \in ℕ$
30	29	a1i	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to 1 \in ℕ$
31	19 30	ffvelrnd	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to i (1) \in ({ℝ^{2}}^{X})$
32		elmapex	$⊢ i (1) \in ({ℝ^{2}}^{X}) \to (ℝ^{2} \in V \land X \in V)$
33	32	simprd	$⊢ i (1) \in ({ℝ^{2}}^{X}) \to X \in V$
34	31 33	syl	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to X \in V$
35	34	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to X \in V$
36		elmapg	$⊢ (ℝ \in V \land X \in V) \to ((l \in X ⟼ 1^{st} (i (n) (l))) \in (ℝ^{X}) \leftrightarrow (l \in X ⟼ 1^{st} (i (n) (l))) : X ⟶ ℝ)$
37	28 35 36	syl2anc	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to ((l \in X ⟼ 1^{st} (i (n) (l))) \in (ℝ^{X}) \leftrightarrow (l \in X ⟼ 1^{st} (i (n) (l))) : X ⟶ ℝ)$
38	26 37	mpbird	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 1^{st} (i (n) (l))) \in (ℝ^{X})$
39	38	fmpttd	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) : ℕ ⟶ ℝ^{X}$
40		id	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to i \in ({({ℝ^{2}}^{X})}^{ℕ})$
41		nnex	$⊢ ℕ \in V$
42	41	mptex	$⊢ (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) \in V$
43	42	a1i	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) \in V$
44	8	fvmpt2	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) \in V) \to F (i) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l))))$
45	40 43 44	syl2anc	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to F (i) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l))))$
46	45	feq1d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (F (i) : ℕ ⟶ ℝ^{X} \leftrightarrow (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) : ℕ ⟶ ℝ^{X})$
47	39 46	mpbird	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to F (i) : ℕ ⟶ ℝ^{X}$
48	47	3ad2ant2	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 F (i) : ℕ ⟶ ℝ^{X}$
49		xp2nd	$⊢ i (n) (l) \in ℝ^{2} \to 2^{nd} (i (n) (l)) \in ℝ$
50	23 49	syl	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land l \in X) \to 2^{nd} (i (n) (l)) \in ℝ$
51	50	fmpttd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 2^{nd} (i (n) (l))) : X ⟶ ℝ$
52		elmapg	$⊢ (ℝ \in V \land X \in V) \to ((l \in X ⟼ 2^{nd} (i (n) (l))) \in (ℝ^{X}) \leftrightarrow (l \in X ⟼ 2^{nd} (i (n) (l))) : X ⟶ ℝ)$
53	28 35 52	syl2anc	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to ((l \in X ⟼ 2^{nd} (i (n) (l))) \in (ℝ^{X}) \leftrightarrow (l \in X ⟼ 2^{nd} (i (n) (l))) : X ⟶ ℝ)$
54	51 53	mpbird	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 2^{nd} (i (n) (l))) \in (ℝ^{X})$
55	54	fmpttd	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) : ℕ ⟶ ℝ^{X}$
56	41	mptex	$⊢ (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) \in V$
57	56	a1i	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) \in V$
58	9	fvmpt2	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) \in V) \to S (i) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l))))$
59	40 57 58	syl2anc	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to S (i) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l))))$
60	59	feq1d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (S (i) : ℕ ⟶ ℝ^{X} \leftrightarrow (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) : ℕ ⟶ ℝ^{X})$
61	55 60	mpbird	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to S (i) : ℕ ⟶ ℝ^{X}$
62	61	3ad2ant2	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 S (i) : ℕ ⟶ ℝ^{X}$
63		simp3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
64	5	a1i	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to I = \underset{k \in X}{⨉} [A (k), B (k))$
65		fveq2	$⊢ j = n \to i (j) = i (n)$
66	65	fveq1d	$⊢ j = n \to i (j) (k) = i (n) (k)$
67	66	fveq2d	$⊢ j = n \to 1^{st} (i (j) (k)) = 1^{st} (i (n) (k))$
68	66	fveq2d	$⊢ j = n \to 2^{nd} (i (j) (k)) = 2^{nd} (i (n) (k))$
69	67 68	oveq12d	$⊢ j = n \to [1^{st} (i (j) (k)), 2^{nd} (i (j) (k))) = [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
70	69	ixpeq2dv	$⊢ j = n \to \underset{k \in X}{⨉} [1^{st} (i (j) (k)), 2^{nd} (i (j) (k))) = \underset{k \in X}{⨉} [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
71	70	cbviunv	$⊢ ⋃_{j \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (j) (k)), 2^{nd} (i (j) (k))) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
72	71	a1i	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (j) (k)), 2^{nd} (i (j) (k))) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
73	19	ffvelrnda	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to i (j) \in ({ℝ^{2}}^{X})$
74		elmapi	$⊢ i (j) \in ({ℝ^{2}}^{X}) \to i (j) : X ⟶ ℝ^{2}$
75	73 74	syl	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to i (j) : X ⟶ ℝ^{2}$
76	75	adantr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \land k \in X) \to i (j) : X ⟶ ℝ^{2}$
77		simpr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \land k \in X) \to k \in X$
78	76 77	fvovco	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \land k \in X) \to ([.) \circ i (j)) (k) = [1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))$
79	78	ixpeq2dva	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} [1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))$
80	79	iuneq2dv	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))$
81		simpl	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to i \in ({({ℝ^{2}}^{X})}^{ℕ})$
82	42	a1i	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) \in V$
83	81 82 44	syl2anc	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to F (i) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l))))$
84	83	fveq1d	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to F (i) (n) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) (n)$
85		simpr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to n \in ℕ$
86		mptexg	$⊢ X \in V \to (l \in X ⟼ 1^{st} (i (n) (l))) \in V$
87	34 86	syl	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (l \in X ⟼ 1^{st} (i (n) (l))) \in V$
88	87	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 1^{st} (i (n) (l))) \in V$
89		eqid	$⊢ (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l))))$
90	89	fvmpt2	$⊢ (n \in ℕ \land (l \in X ⟼ 1^{st} (i (n) (l))) \in V) \to (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) (n) = (l \in X ⟼ 1^{st} (i (n) (l)))$
91	85 88 90	syl2anc	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))) (n) = (l \in X ⟼ 1^{st} (i (n) (l)))$
92	84 91	eqtrd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to F (i) (n) = (l \in X ⟼ 1^{st} (i (n) (l)))$
93	92	fveq1d	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to F (i) (n) (k) = (l \in X ⟼ 1^{st} (i (n) (l))) (k)$
94	93	adantr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to F (i) (n) (k) = (l \in X ⟼ 1^{st} (i (n) (l))) (k)$
95		eqidd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to (l \in X ⟼ 1^{st} (i (n) (l))) = (l \in X ⟼ 1^{st} (i (n) (l)))$
96		simpr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \land l = k) \to l = k$
97	96	fveq2d	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \land l = k) \to i (n) (l) = i (n) (k)$
98	97	fveq2d	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \land l = k) \to 1^{st} (i (n) (l)) = 1^{st} (i (n) (k))$
99		simpr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to k \in X$
100		fvexd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to 1^{st} (i (n) (k)) \in V$
101	95 98 99 100	fvmptd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to (l \in X ⟼ 1^{st} (i (n) (l))) (k) = 1^{st} (i (n) (k))$
102	101	adantlr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to (l \in X ⟼ 1^{st} (i (n) (l))) (k) = 1^{st} (i (n) (k))$
103	94 102	eqtrd	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to F (i) (n) (k) = 1^{st} (i (n) (k))$
104	59	fveq1d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to S (i) (n) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) (n)$
105	104	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to S (i) (n) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) (n)$
106		mptexg	$⊢ X \in V \to (l \in X ⟼ 2^{nd} (i (n) (l))) \in V$
107	34 106	syl	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (l \in X ⟼ 2^{nd} (i (n) (l))) \in V$
108	107	adantr	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (l \in X ⟼ 2^{nd} (i (n) (l))) \in V$
109		eqid	$⊢ (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l))))$
110	109	fvmpt2	$⊢ (n \in ℕ \land (l \in X ⟼ 2^{nd} (i (n) (l))) \in V) \to (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) (n) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
111	85 108 110	syl2anc	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))) (n) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
112	105 111	eqtrd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to S (i) (n) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
113	112	fveq1d	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to S (i) (n) (k) = (l \in X ⟼ 2^{nd} (i (n) (l))) (k)$
114	113	adantr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to S (i) (n) (k) = (l \in X ⟼ 2^{nd} (i (n) (l))) (k)$
115		eqidd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to (l \in X ⟼ 2^{nd} (i (n) (l))) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
116		2fveq3	$⊢ l = k \to 2^{nd} (i (n) (l)) = 2^{nd} (i (n) (k))$
117	116	adantl	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \land l = k) \to 2^{nd} (i (n) (l)) = 2^{nd} (i (n) (k))$
118		fvexd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to 2^{nd} (i (n) (k)) \in V$
119	115 117 99 118	fvmptd	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land k \in X) \to (l \in X ⟼ 2^{nd} (i (n) (l))) (k) = 2^{nd} (i (n) (k))$
120	119	adantlr	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to (l \in X ⟼ 2^{nd} (i (n) (l))) (k) = 2^{nd} (i (n) (k))$
121	114 120	eqtrd	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to S (i) (n) (k) = 2^{nd} (i (n) (k))$
122	103 121	oveq12d	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \land k \in X) \to [F (i) (n) (k), S (i) (n) (k)) = [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
123	122	ixpeq2dva	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land n \in ℕ) \to \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k)) = \underset{k \in X}{⨉} [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
124	123	iuneq2dv	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k)) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [1^{st} (i (n) (k)), 2^{nd} (i (n) (k)))$
125	72 80 124	3eqtr4d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k))$
126	125	adantl	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k))$
127	126	3adant3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) = ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k))$
128	64 127	sseq12d	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k)))$
129	63 128	mpbid	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)) \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k))$
130	129	3adant3r	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ⋃_{n \in ℕ} \underset{k \in X}{⨉} [F (i) (n) (k), S (i) (n) (k))$
131	6 16 17 18 48 62 130	hoidmvle	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 L (X) B \leq sum^((n \in ℕ ⟼ F (i) (n) L (X) S (i) (n)))$
132		simpl	$⊢ (n = j \land l \in X) \to n = j$
133	132	fveq2d	$⊢ (n = j \land l \in X) \to i (n) = i (j)$
134	133	fveq1d	$⊢ (n = j \land l \in X) \to i (n) (l) = i (j) (l)$
135	134	fveq2d	$⊢ (n = j \land l \in X) \to 1^{st} (i (n) (l)) = 1^{st} (i (j) (l))$
136	135	mpteq2dva	$⊢ n = j \to (l \in X ⟼ 1^{st} (i (n) (l))) = (l \in X ⟼ 1^{st} (i (j) (l)))$
137	136	fveq1d	$⊢ n = j \to (l \in X ⟼ 1^{st} (i (n) (l))) (k) = (l \in X ⟼ 1^{st} (i (j) (l))) (k)$
138	137	adantr	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 1^{st} (i (n) (l))) (k) = (l \in X ⟼ 1^{st} (i (j) (l))) (k)$
139		eqidd	$⊢ k \in X \to (l \in X ⟼ 1^{st} (i (j) (l))) = (l \in X ⟼ 1^{st} (i (j) (l)))$
140		2fveq3	$⊢ l = k \to 1^{st} (i (j) (l)) = 1^{st} (i (j) (k))$
141	140	adantl	$⊢ (k \in X \land l = k) \to 1^{st} (i (j) (l)) = 1^{st} (i (j) (k))$
142		id	$⊢ k \in X \to k \in X$
143		fvexd	$⊢ k \in X \to 1^{st} (i (j) (k)) \in V$
144	139 141 142 143	fvmptd	$⊢ k \in X \to (l \in X ⟼ 1^{st} (i (j) (l))) (k) = 1^{st} (i (j) (k))$
145	144	adantl	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 1^{st} (i (j) (l))) (k) = 1^{st} (i (j) (k))$
146	138 145	eqtrd	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 1^{st} (i (n) (l))) (k) = 1^{st} (i (j) (k))$
147	134	fveq2d	$⊢ (n = j \land l \in X) \to 2^{nd} (i (n) (l)) = 2^{nd} (i (j) (l))$
148	147	mpteq2dva	$⊢ n = j \to (l \in X ⟼ 2^{nd} (i (n) (l))) = (l \in X ⟼ 2^{nd} (i (j) (l)))$
149	148	fveq1d	$⊢ n = j \to (l \in X ⟼ 2^{nd} (i (n) (l))) (k) = (l \in X ⟼ 2^{nd} (i (j) (l))) (k)$
150	149	adantr	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 2^{nd} (i (n) (l))) (k) = (l \in X ⟼ 2^{nd} (i (j) (l))) (k)$
151		eqidd	$⊢ k \in X \to (l \in X ⟼ 2^{nd} (i (j) (l))) = (l \in X ⟼ 2^{nd} (i (j) (l)))$
152		2fveq3	$⊢ l = k \to 2^{nd} (i (j) (l)) = 2^{nd} (i (j) (k))$
153	152	adantl	$⊢ (k \in X \land l = k) \to 2^{nd} (i (j) (l)) = 2^{nd} (i (j) (k))$
154		fvexd	$⊢ k \in X \to 2^{nd} (i (j) (k)) \in V$
155	151 153 142 154	fvmptd	$⊢ k \in X \to (l \in X ⟼ 2^{nd} (i (j) (l))) (k) = 2^{nd} (i (j) (k))$
156	155	adantl	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 2^{nd} (i (j) (l))) (k) = 2^{nd} (i (j) (k))$
157	150 156	eqtrd	$⊢ (n = j \land k \in X) \to (l \in X ⟼ 2^{nd} (i (n) (l))) (k) = 2^{nd} (i (j) (k))$
158	146 157	oveq12d	$⊢ (n = j \land k \in X) \to [(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)) = [1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))$
159	158	fveq2d	$⊢ (n = j \land k \in X) \to vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k))) = vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k))))$
160	159	prodeq2dv	$⊢ n = j \to \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k))) = \prod_{k \in X} vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k))))$
161	160	cbvmptv	$⊢ (n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))) = (j \in ℕ ⟼ \prod_{k \in X} vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))))$
162	161	a1i	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))) = (j \in ℕ ⟼ \prod_{k \in X} vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))))$
163	78	eqcomd	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \land k \in X) \to [1^{st} (i (j) (k)), 2^{nd} (i (j) (k))) = ([.) \circ i (j)) (k)$
164	163	fveq2d	$⊢ ((i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \land k \in X) \to vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))) = vol (([.) \circ i (j)) (k))$
165	164	prodeq2dv	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land j \in ℕ) \to \prod_{k \in X} vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k)))) = \prod_{k \in X} vol (([.) \circ i (j)) (k))$
166	165	mpteq2dva	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (j \in ℕ ⟼ \prod_{k \in X} vol ([1^{st} (i (j) (k)), 2^{nd} (i (j) (k))))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
167	162 166	eqtrd	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to (n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
168	167	fveq2d	$⊢ i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to sum^((n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k))))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
169	168	3ad2ant2	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k))))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
170	92	adantll	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to F (i) (n) = (l \in X ⟼ 1^{st} (i (n) (l)))$
171	112	adantll	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to S (i) (n) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
172	170 171	oveq12d	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to F (i) (n) L (X) S (i) (n) = (l \in X ⟼ 1^{st} (i (n) (l))) L (X) (l \in X ⟼ 2^{nd} (i (n) (l)))$
173	1	ad2antrr	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to X \in Fin$
174	2	ad2antrr	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to X \neq \emptyset$
175	23	adantlll	$⊢ (((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \land l \in X) \to i (n) (l) \in ℝ^{2}$
176	175 24	syl	$⊢ (((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \land l \in X) \to 1^{st} (i (n) (l)) \in ℝ$
177	176	fmpttd	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to (l \in X ⟼ 1^{st} (i (n) (l))) : X ⟶ ℝ$
178	175 49	syl	$⊢ (((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \land l \in X) \to 2^{nd} (i (n) (l)) \in ℝ$
179	178	fmpttd	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to (l \in X ⟼ 2^{nd} (i (n) (l))) : X ⟶ ℝ$
180	6 173 174 177 179	hoidmvn0val	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to (l \in X ⟼ 1^{st} (i (n) (l))) L (X) (l \in X ⟼ 2^{nd} (i (n) (l))) = \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))$
181	172 180	eqtrd	$⊢ ((φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \land n \in ℕ) \to F (i) (n) L (X) S (i) (n) = \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))$
182	181	mpteq2dva	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to (n \in ℕ ⟼ F (i) (n) L (X) S (i) (n)) = (n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k))))$
183	182	fveq2d	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ})) \to sum^((n \in ℕ ⟼ F (i) (n) L (X) S (i) (n))) = sum^((n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))))$
184	183	3adant3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((n \in ℕ ⟼ F (i) (n) L (X) S (i) (n))) = sum^((n \in ℕ ⟼ \prod_{k \in X} vol ([(l \in X ⟼ 1^{st} (i (n) (l))) (k), (l \in X ⟼ 2^{nd} (i (n) (l))) (k)))))$
185		simp3	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land 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))))$
186	169 184 185	3eqtr4d	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to sum^((n \in ℕ ⟼ F (i) (n) L (X) S (i) (n))) = z$
187	186	3adant3l	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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^((n \in ℕ ⟼ F (i) (n) L (X) S (i) (n))) = z$
188	131 187	breqtrd	$⊢ (φ \land i \in ({({ℝ^{2}}^{X})}^{ℕ}) \land (I \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 L (X) B \leq z$
189	188	3exp	$⊢ φ \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ((I \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 L (X) B \leq z))$
190	189	adantr	$⊢ (φ \land z \in M) \to (i \in ({({ℝ^{2}}^{X})}^{ℕ}) \to ((I \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 L (X) B \leq z))$
191	190	rexlimdv	$⊢ (φ \land z \in M) \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 L (X) B \leq z)$
192	15 191	mpd	$⊢ (φ \land z \in M) \to A L (X) B \leq z$
193	192	ralrimiva	$⊢ φ \to \forall z \in M A L (X) B \leq z$
194		ssrab2	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \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 ℝ^{}$
195	7 194	eqsstri	$⊢ M \subseteq ℝ^{*}$
196	195	a1i	$⊢ φ \to M \subseteq ℝ^{*}$
197		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
198	6 1 3 4	hoidmvcl	$⊢ φ \to A L (X) B \in [0, +∞)$
199	197 198	sselid	$⊢ φ \to A L (X) B \in ℝ^{*}$
200		infxrgelb	$⊢ (M \subseteq ℝ^{} \land A L (X) B \in ℝ^{}) \to (A L (X) B \leq sup (M ℝ^{*} <) \leftrightarrow \forall z \in M A L (X) B \leq z)$
201	196 199 200	syl2anc	$⊢ φ \to (A L (X) B \leq sup (M ℝ^{*} <) \leftrightarrow \forall z \in M A L (X) B \leq z)$
202	193 201	mpbird	$⊢ φ \to A L (X) B \leq sup (M ℝ^{*} <)$
203	5	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} [A (k), B (k))$
204		nfv	$⊢ Ⅎ k φ$
205	3	ffvelrnda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
206	4	ffvelrnda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
207	206	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
208	204 205 207	hoissrrn2	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ℝ^{X}$
209	203 208	eqsstrd	$⊢ φ \to I \subseteq ℝ^{X}$
210	1 2 209 7	ovnn0val	$⊢ φ \to voln* (X) (I) = sup (M ℝ^{*} <)$
211	210	eqcomd	$⊢ φ \to sup (M ℝ^{} <) = voln (X) (I)$
212	202 211	breqtrd	$⊢ φ \to A L (X) B \leq voln* (X) (I)$

Metamath Proof Explorer

Theorem ovnhoilem2

Proof