vonioo

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

	Ref	Expression
Hypotheses	vonioo.x	$⊢ φ \to X \in Fin$
	vonioo.a	$⊢ φ \to A : X ⟶ ℝ$
	vonioo.b	$⊢ φ \to B : X ⟶ ℝ$
	vonioo.i	$⊢ I = \underset{k \in X}{⨉} (A (k), B (k))$
	vonioo.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	vonioo	$⊢ φ \to voln (X) (I) = A L (X) B$

Proof

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

Metamath Proof Explorer

Theorem vonioo

Proof