vonicc

Description: The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonicc.x	$⊢ φ \to X \in Fin$
	vonicc.a	$⊢ φ \to A : X ⟶ ℝ$
	vonicc.b	$⊢ φ \to B : X ⟶ ℝ$
	vonicc.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k)]$
	vonicc.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
Assertion	vonicc	$⊢ φ \to voln (X) (I) = A L (X) B$

Proof

Step	Hyp	Ref	Expression
1		vonicc.x	$⊢ φ \to X \in Fin$
2		vonicc.a	$⊢ φ \to A : X ⟶ ℝ$
3		vonicc.b	$⊢ φ \to B : X ⟶ ℝ$
4		vonicc.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k)]$
5		vonicc.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
6	2	adantr	$⊢ (φ \land X = \emptyset) \to A : X ⟶ ℝ$
7		feq2	$⊢ X = \emptyset \to (A : X ⟶ ℝ \leftrightarrow A : \emptyset ⟶ ℝ)$
8	7	adantl	$⊢ (φ \land X = \emptyset) \to (A : X ⟶ ℝ \leftrightarrow A : \emptyset ⟶ ℝ)$
9	6 8	mpbid	$⊢ (φ \land X = \emptyset) \to A : \emptyset ⟶ ℝ$
10	3	adantr	$⊢ (φ \land X = \emptyset) \to B : X ⟶ ℝ$
11		feq2	$⊢ X = \emptyset \to (B : X ⟶ ℝ \leftrightarrow B : \emptyset ⟶ ℝ)$
12	11	adantl	$⊢ (φ \land X = \emptyset) \to (B : X ⟶ ℝ \leftrightarrow B : \emptyset ⟶ ℝ)$
13	10 12	mpbid	$⊢ (φ \land X = \emptyset) \to B : \emptyset ⟶ ℝ$
14	5 9 13	hoidmv0val	$⊢ (φ \land X = \emptyset) \to A L (\emptyset) B = 0$
15	14	eqcomd	$⊢ (φ \land X = \emptyset) \to 0 = A L (\emptyset) B$
16		fveq2	$⊢ X = \emptyset \to voln (X) = voln (\emptyset)$
17	4	a1i	$⊢ X = \emptyset \to I = \underset{k \in X}{⨉} [A (k), B (k)]$
18		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)] = \underset{k \in \emptyset}{⨉} [A (k), B (k)]$
19	17 18	eqtrd	$⊢ X = \emptyset \to I = \underset{k \in \emptyset}{⨉} [A (k), B (k)]$
20	16 19	fveq12d	$⊢ X = \emptyset \to voln (X) (I) = voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)])$
21	20	adantl	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)])$
22		0fin	$⊢ \emptyset \in Fin$
23	22	a1i	$⊢ (φ \land X = \emptyset) \to \emptyset \in Fin$
24		eqid	$⊢ dom voln (\emptyset) = dom voln (\emptyset)$
25	23 24 9 13	iccvonmbl	$⊢ (φ \land X = \emptyset) \to \underset{k \in \emptyset}{⨉} [A (k), B (k)] \in dom voln (\emptyset)$
26	25	von0val	$⊢ (φ \land X = \emptyset) \to voln (\emptyset) (\underset{k \in \emptyset}{⨉} [A (k), B (k)]) = 0$
27	21 26	eqtrd	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = 0$
28		fveq2	$⊢ X = \emptyset \to L (X) = L (\emptyset)$
29	28	oveqd	$⊢ X = \emptyset \to A L (X) B = A L (\emptyset) B$
30	29	adantl	$⊢ (φ \land X = \emptyset) \to A L (X) B = A L (\emptyset) B$
31	15 27 30	3eqtr4d	$⊢ (φ \land X = \emptyset) \to voln (X) (I) = A L (X) B$
32		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
33	32	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
34		nfv	$⊢ Ⅎ k (φ \land X \neq \emptyset)$
35		nfra1	$⊢ Ⅎ k \forall k \in X A (k) \leq B (k)$
36	34 35	nfan	$⊢ Ⅎ k ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k))$
37	2	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
38	3	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
39		volico2	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
40	37 38 39	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
41	40	ad4ant14	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to vol ([A (k), B (k))) = if (A (k) \leq B (k), B (k) - A (k), 0)$
42		rspa	$⊢ (\forall k \in X A (k) \leq B (k) \land k \in X) \to A (k) \leq B (k)$
43	42	iftrued	$⊢ (\forall k \in X A (k) \leq B (k) \land k \in X) \to if (A (k) \leq B (k), B (k) - A (k), 0) = B (k) - A (k)$
44	43	adantll	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to if (A (k) \leq B (k), B (k) - A (k), 0) = B (k) - A (k)$
45	41 44	eqtrd	$⊢ (((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \land k \in X) \to vol ([A (k), B (k))) = B (k) - A (k)$
46	45	ex	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to (k \in X \to vol ([A (k), B (k))) = B (k) - A (k))$
47	36 46	ralrimi	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \forall k \in X vol ([A (k), B (k))) = B (k) - A (k)$
48	47	prodeq2d	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in X} (B (k) - A (k))$
49	48	eqcomd	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \prod_{k \in X} (B (k) - A (k)) = \prod_{k \in X} vol ([A (k), B (k)))$
50		fveq2	$⊢ k = j \to A (k) = A (j)$
51		fveq2	$⊢ k = j \to B (k) = B (j)$
52	50 51	breq12d	$⊢ k = j \to (A (k) \leq B (k) \leftrightarrow A (j) \leq B (j))$
53	52	cbvralvw	$⊢ \forall k \in X A (k) \leq B (k) \leftrightarrow \forall j \in X A (j) \leq B (j)$
54	53	biimpi	$⊢ \forall k \in X A (k) \leq B (k) \to \forall j \in X A (j) \leq B (j)$
55	54	adantl	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to \forall j \in X A (j) \leq B (j)$
56	1	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
57	56	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to X \in Fin$
58	2	adantr	$⊢ (φ \land X \neq \emptyset) \to A : X ⟶ ℝ$
59	58	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to A : X ⟶ ℝ$
60	3	adantr	$⊢ (φ \land X \neq \emptyset) \to B : X ⟶ ℝ$
61	60	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to B : X ⟶ ℝ$
62		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
63	62	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to X \neq \emptyset$
64	53 42	sylanbr	$⊢ (\forall j \in X A (j) \leq B (j) \land k \in X) \to A (k) \leq B (k)$
65	64	adantll	$⊢ (((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \land k \in X) \to A (k) \leq B (k)$
66		fveq2	$⊢ j = k \to B (j) = B (k)$
67	66	oveq1d	$⊢ j = k \to B (j) + (\frac{1}{m}) = B (k) + (\frac{1}{m})$
68	67	cbvmptv	$⊢ (j \in X ⟼ B (j) + (\frac{1}{m})) = (k \in X ⟼ B (k) + (\frac{1}{m}))$
69	68	mpteq2i	$⊢ (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) = (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m})))$
70		oveq2	$⊢ m = n \to \frac{1}{m} = \frac{1}{n}$
71	70	oveq2d	$⊢ m = n \to B (k) + (\frac{1}{m}) = B (k) + (\frac{1}{n})$
72	71	mpteq2dv	$⊢ m = n \to (k \in X ⟼ B (k) + (\frac{1}{m})) = (k \in X ⟼ B (k) + (\frac{1}{n}))$
73	72	cbvmptv	$⊢ (m \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{m}))) = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
74	69 73	eqtri	$⊢ (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) = (n \in ℕ ⟼ (k \in X ⟼ B (k) + (\frac{1}{n})))$
75		fveq2	$⊢ i = n \to (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) = (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n)$
76	75	fveq1d	$⊢ i = n \to (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k) = (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k)$
77	76	oveq2d	$⊢ i = n \to [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k)) = [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k))$
78	77	ixpeq2dv	$⊢ i = n \to \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k)) = \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k))$
79	78	cbvmptv	$⊢ (i \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (i) (k))) = (n \in ℕ ⟼ \underset{k \in X}{⨉} [A (k), (m \in ℕ ⟼ (j \in X ⟼ B (j) + (\frac{1}{m}))) (n) (k)))$
80	57 59 61 63 65 4 74 79	vonicclem2	$⊢ ((φ \land X \neq \emptyset) \land \forall j \in X A (j) \leq B (j)) \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$
81	55 80	syldan	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = \prod_{k \in X} (B (k) - A (k))$
82	5 56 62 58 60	hoidmvn0val	$⊢ (φ \land X \neq \emptyset) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
83	82	adantr	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
84	49 81 83	3eqtr4d	$⊢ ((φ \land X \neq \emptyset) \land \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = A L (X) B$
85		rexnal	$⊢ \exists k \in X \neg A (k) \leq B (k) \leftrightarrow \neg \forall k \in X A (k) \leq B (k)$
86	85	bicomi	$⊢ \neg \forall k \in X A (k) \leq B (k) \leftrightarrow \exists k \in X \neg A (k) \leq B (k)$
87	86	biimpi	$⊢ \neg \forall k \in X A (k) \leq B (k) \to \exists k \in X \neg A (k) \leq B (k)$
88	87	adantl	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X \neg A (k) \leq B (k)$
89		simpr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to \neg A (k) \leq B (k)$
90	38	adantr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to B (k) \in ℝ$
91	37	adantr	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to A (k) \in ℝ$
92	90 91	ltnled	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to (B (k) < A (k) \leftrightarrow \neg A (k) \leq B (k))$
93	89 92	mpbird	$⊢ ((φ \land k \in X) \land \neg A (k) \leq B (k)) \to B (k) < A (k)$
94	93	ex	$⊢ (φ \land k \in X) \to (\neg A (k) \leq B (k) \to B (k) < A (k))$
95	94	reximdva	$⊢ φ \to (\exists k \in X \neg A (k) \leq B (k) \to \exists k \in X B (k) < A (k))$
96	95	adantr	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to (\exists k \in X \neg A (k) \leq B (k) \to \exists k \in X B (k) < A (k))$
97	88 96	mpd	$⊢ (φ \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X B (k) < A (k)$
98	97	adantlr	$⊢ ((φ \land X \neq \emptyset) \land \neg \forall k \in X A (k) \leq B (k)) \to \exists k \in X B (k) < A (k)$
99		nfcv	$⊢ \underline{Ⅎ} k voln (X)$
100		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} [A (k), B (k)]$
101	4 100	nfcxfr	$⊢ \underline{Ⅎ} k I$
102	99 101	nffv	$⊢ \underline{Ⅎ} k voln (X) (I)$
103		nfcv	$⊢ \underline{Ⅎ} k A$
104		nfcv	$⊢ \underline{Ⅎ} k Fin$
105		nfcv	$⊢ \underline{Ⅎ} k (ℝ^{x})$
106		nfv	$⊢ Ⅎ k x = \emptyset$
107		nfcv	$⊢ \underline{Ⅎ} k 0$
108		nfcv	$⊢ \underline{Ⅎ} k x$
109	108	nfcprod1	$⊢ \underline{Ⅎ} k \prod_{k \in x} vol ([a (k), b (k)))$
110	106 107 109	nfif	$⊢ \underline{Ⅎ} k if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))$
111	105 105 110	nfmpo	$⊢ \underline{Ⅎ} k (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))$
112	104 111	nfmpt	$⊢ \underline{Ⅎ} k (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
113	5 112	nfcxfr	$⊢ \underline{Ⅎ} k L$
114		nfcv	$⊢ \underline{Ⅎ} k X$
115	113 114	nffv	$⊢ \underline{Ⅎ} k L (X)$
116		nfcv	$⊢ \underline{Ⅎ} k B$
117	103 115 116	nfov	$⊢ \underline{Ⅎ} k (A L (X) B)$
118	102 117	nfeq	$⊢ Ⅎ k voln (X) (I) = A L (X) B$
119	1	vonmea	$⊢ φ \to voln (X) \in Meas$
120	119	mea0	$⊢ φ \to voln (X) (\emptyset) = 0$
121	120	3ad2ant1	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (\emptyset) = 0$
122	4	a1i	$⊢ (φ \land k \in X \land B (k) < A (k)) \to I = \underset{k \in X}{⨉} [A (k), B (k)]$
123		simp2	$⊢ (φ \land k \in X \land B (k) < A (k)) \to k \in X$
124		simp3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to B (k) < A (k)$
125		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
126	125 37	sselid	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
127	125 38	sselid	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
128		icc0	$⊢ (A (k) \in ℝ^{} \land B (k) \in ℝ^{}) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
129	126 127 128	syl2anc	$⊢ (φ \land k \in X) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
130	129	3adant3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to ([A (k), B (k)] = \emptyset \leftrightarrow B (k) < A (k))$
131	124 130	mpbird	$⊢ (φ \land k \in X \land B (k) < A (k)) \to [A (k), B (k)] = \emptyset$
132		rspe	$⊢ (k \in X \land [A (k), B (k)] = \emptyset) \to \exists k \in X [A (k), B (k)] = \emptyset$
133	123 131 132	syl2anc	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \exists k \in X [A (k), B (k)] = \emptyset$
134		ixp0	$⊢ \exists k \in X [A (k), B (k)] = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)] = \emptyset$
135	133 134	syl	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \underset{k \in X}{⨉} [A (k), B (k)] = \emptyset$
136	122 135	eqtrd	$⊢ (φ \land k \in X \land B (k) < A (k)) \to I = \emptyset$
137	136	fveq2d	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (I) = voln (X) (\emptyset)$
138		ne0i	$⊢ k \in X \to X \neq \emptyset$
139	138	adantl	$⊢ (φ \land k \in X) \to X \neq \emptyset$
140	139 82	syldan	$⊢ (φ \land k \in X) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
141	140	3adant3	$⊢ (φ \land k \in X \land B (k) < A (k)) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
142		eleq1w	$⊢ j = k \to (j \in X \leftrightarrow k \in X)$
143		fveq2	$⊢ j = k \to A (j) = A (k)$
144	66 143	breq12d	$⊢ j = k \to (B (j) < A (j) \leftrightarrow B (k) < A (k))$
145	142 144	3anbi23d	$⊢ j = k \to ((φ \land j \in X \land B (j) < A (j)) \leftrightarrow (φ \land k \in X \land B (k) < A (k)))$
146	145	imbi1d	$⊢ j = k \to (((φ \land j \in X \land B (j) < A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0) \leftrightarrow ((φ \land k \in X \land B (k) < A (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0))$
147		nfv	$⊢ Ⅎ k (φ \land j \in X \land B (j) < A (j))$
148	1	3ad2ant1	$⊢ (φ \land j \in X \land B (j) < A (j)) \to X \in Fin$
149		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
150	37 38 149	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
151	150	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
152	151	3ad2antl1	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
153		simp2	$⊢ (φ \land j \in X \land B (j) < A (j)) \to j \in X$
154	50 51	oveq12d	$⊢ k = j \to [A (k), B (k)) = [A (j), B (j))$
155	154	fveq2d	$⊢ k = j \to vol ([A (k), B (k))) = vol ([A (j), B (j)))$
156	155	adantl	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (k), B (k))) = vol ([A (j), B (j)))$
157	2	ffvelcdmda	$⊢ (φ \land j \in X) \to A (j) \in ℝ$
158	3	ffvelcdmda	$⊢ (φ \land j \in X) \to B (j) \in ℝ$
159		volico2	$⊢ (A (j) \in ℝ \land B (j) \in ℝ) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
160	157 158 159	syl2anc	$⊢ (φ \land j \in X) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
161	160	3adant3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to vol ([A (j), B (j))) = if (A (j) \leq B (j), B (j) - A (j), 0)$
162		simp3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to B (j) < A (j)$
163	158 157	ltnled	$⊢ (φ \land j \in X) \to (B (j) < A (j) \leftrightarrow \neg A (j) \leq B (j))$
164	163	3adant3	$⊢ (φ \land j \in X \land B (j) < A (j)) \to (B (j) < A (j) \leftrightarrow \neg A (j) \leq B (j))$
165	162 164	mpbid	$⊢ (φ \land j \in X \land B (j) < A (j)) \to \neg A (j) \leq B (j)$
166	165	iffalsed	$⊢ (φ \land j \in X \land B (j) < A (j)) \to if (A (j) \leq B (j), B (j) - A (j), 0) = 0$
167	161 166	eqtrd	$⊢ (φ \land j \in X \land B (j) < A (j)) \to vol ([A (j), B (j))) = 0$
168	167	adantr	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (j), B (j))) = 0$
169	156 168	eqtrd	$⊢ ((φ \land j \in X \land B (j) < A (j)) \land k = j) \to vol ([A (k), B (k))) = 0$
170	147 148 152 153 169	fprodeq0g	$⊢ (φ \land j \in X \land B (j) < A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
171	146 170	chvarvv	$⊢ (φ \land k \in X \land B (k) < A (k)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
172	141 171	eqtrd	$⊢ (φ \land k \in X \land B (k) < A (k)) \to A L (X) B = 0$
173	121 137 172	3eqtr4d	$⊢ (φ \land k \in X \land B (k) < A (k)) \to voln (X) (I) = A L (X) B$
174	173	3exp	$⊢ φ \to (k \in X \to (B (k) < A (k) \to voln (X) (I) = A L (X) B))$
175	174	adantr	$⊢ (φ \land X \neq \emptyset) \to (k \in X \to (B (k) < A (k) \to voln (X) (I) = A L (X) B))$
176	34 118 175	rexlimd	$⊢ (φ \land X \neq \emptyset) \to (\exists k \in X B (k) < A (k) \to voln (X) (I) = A L (X) B)$
177	176	imp	$⊢ ((φ \land X \neq \emptyset) \land \exists k \in X B (k) < A (k)) \to voln (X) (I) = A L (X) B$
178	98 177	syldan	$⊢ ((φ \land X \neq \emptyset) \land \neg \forall k \in X A (k) \leq B (k)) \to voln (X) (I) = A L (X) B$
179	84 178	pm2.61dan	$⊢ (φ \land X \neq \emptyset) \to voln (X) (I) = A L (X) B$
180	33 179	syldan	$⊢ (φ \land \neg X = \emptyset) \to voln (X) (I) = A L (X) B$
181	31 180	pm2.61dan	$⊢ φ \to voln (X) (I) = A L (X) B$

Metamath Proof Explorer

Theorem vonicc

Proof