ovnhoi

Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ovnhoi.x	$⊢ φ \to X \in Fin$
2		ovnhoi.a	$⊢ φ \to A : X ⟶ ℝ$
3		ovnhoi.b	$⊢ φ \to B : X ⟶ ℝ$
4		ovnhoi.c	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
5		ovnhoi.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	4	a1i	$⊢ φ \to I = \underset{k \in X}{⨉} [A (k), B (k))$
7		nfv	$⊢ Ⅎ k φ$
8	2	ffvelrnda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
9	3	ffvelrnda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
10	9	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
11	7 8 10	hoissrrn2	$⊢ φ \to \underset{k \in X}{⨉} [A (k), B (k)) \subseteq ℝ^{X}$
12	6 11	eqsstrd	$⊢ φ \to I \subseteq ℝ^{X}$
13	1 12	ovnxrcl	$⊢ φ \to voln* (X) (I) \in ℝ^{*}$
14		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
15	5 1 2 3	hoidmvcl	$⊢ φ \to A L (X) B \in [0, +∞)$
16	14 15	sseldi	$⊢ φ \to A L (X) B \in ℝ^{*}$
17		fveq2	$⊢ X = \emptyset \to voln* (X) = voln* (\emptyset)$
18	17	fveq1d	$⊢ X = \emptyset \to voln* (X) (I) = voln* (\emptyset) (I)$
19	18	adantl	$⊢ (φ \land X = \emptyset) \to voln* (X) (I) = voln* (\emptyset) (I)$
20		ixpeq1	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)) = \underset{k \in \emptyset}{⨉} [A (k), B (k))$
21		ixp0x	$⊢ \underset{k \in \emptyset}{⨉} [A (k), B (k)) = \{\emptyset\}$
22	21	a1i	$⊢ X = \emptyset \to \underset{k \in \emptyset}{⨉} [A (k), B (k)) = \{\emptyset\}$
23	20 22	eqtrd	$⊢ X = \emptyset \to \underset{k \in X}{⨉} [A (k), B (k)) = \{\emptyset\}$
24	23	adantl	$⊢ (φ \land X = \emptyset) \to \underset{k \in X}{⨉} [A (k), B (k)) = \{\emptyset\}$
25	4	a1i	$⊢ (φ \land X = \emptyset) \to I = \underset{k \in X}{⨉} [A (k), B (k))$
26		reex	$⊢ ℝ \in V$
27		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
28	26 27	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
29	28	a1i	$⊢ (φ \land X = \emptyset) \to ℝ^{\emptyset} = \{\emptyset\}$
30	24 25 29	3eqtr4d	$⊢ (φ \land X = \emptyset) \to I = ℝ^{\emptyset}$
31		eqimss	$⊢ I = ℝ^{\emptyset} \to I \subseteq ℝ^{\emptyset}$
32	30 31	syl	$⊢ (φ \land X = \emptyset) \to I \subseteq ℝ^{\emptyset}$
33	32	ovn0val	$⊢ (φ \land X = \emptyset) \to voln* (\emptyset) (I) = 0$
34	19 33	eqtrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (I) = 0$
35		0red	$⊢ (φ \land X = \emptyset) \to 0 \in ℝ$
36	34 35	eqeltrd	$⊢ (φ \land X = \emptyset) \to voln* (X) (I) \in ℝ$
37		eqidd	$⊢ (φ \land X = \emptyset) \to 0 = 0$
38		fveq2	$⊢ X = \emptyset \to L (X) = L (\emptyset)$
39	38	oveqd	$⊢ X = \emptyset \to A L (X) B = A L (\emptyset) B$
40	39	adantl	$⊢ (φ \land X = \emptyset) \to A L (X) B = A L (\emptyset) B$
41	2	adantr	$⊢ (φ \land X = \emptyset) \to A : X ⟶ ℝ$
42		simpr	$⊢ (φ \land X = \emptyset) \to X = \emptyset$
43	42	feq2d	$⊢ (φ \land X = \emptyset) \to (A : X ⟶ ℝ \leftrightarrow A : \emptyset ⟶ ℝ)$
44	41 43	mpbid	$⊢ (φ \land X = \emptyset) \to A : \emptyset ⟶ ℝ$
45	3	adantr	$⊢ (φ \land X = \emptyset) \to B : X ⟶ ℝ$
46	42	feq2d	$⊢ (φ \land X = \emptyset) \to (B : X ⟶ ℝ \leftrightarrow B : \emptyset ⟶ ℝ)$
47	45 46	mpbid	$⊢ (φ \land X = \emptyset) \to B : \emptyset ⟶ ℝ$
48	5 44 47	hoidmv0val	$⊢ (φ \land X = \emptyset) \to A L (\emptyset) B = 0$
49	40 48	eqtrd	$⊢ (φ \land X = \emptyset) \to A L (X) B = 0$
50	37 34 49	3eqtr4d	$⊢ (φ \land X = \emptyset) \to voln* (X) (I) = A L (X) B$
51	36 50	eqled	$⊢ (φ \land X = \emptyset) \to voln* (X) (I) \leq A L (X) B$
52		eqid	$⊢ \{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)))))\} = \{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)))))\}$
53		eqeq1	$⊢ n = j \to (n = 1 \leftrightarrow j = 1)$
54	53	ifbid	$⊢ n = j \to if (n = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩) = if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)$
55	54	mpteq2dv	$⊢ n = j \to (k \in X ⟼ if (n = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)) = (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩))$
56	55	cbvmptv	$⊢ (n \in ℕ ⟼ (k \in X ⟼ if (n = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩))) = (j \in ℕ ⟼ (k \in X ⟼ if (j = 1, ⟨A (k), B (k)⟩, ⟨0, 0⟩)))$
57	1 2 3 4 52 56	ovnhoilem1	$⊢ φ \to voln* (X) (I) \leq \prod_{k \in X} vol ([A (k), B (k)))$
58	57	adantr	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (I) \leq \prod_{k \in X} vol ([A (k), B (k)))$
59	1	adantr	$⊢ (φ \land \neg X = \emptyset) \to X \in Fin$
60		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
61	60	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
62	2	adantr	$⊢ (φ \land \neg X = \emptyset) \to A : X ⟶ ℝ$
63	3	adantr	$⊢ (φ \land \neg X = \emptyset) \to B : X ⟶ ℝ$
64	5 59 61 62 63	hoidmvn0val	$⊢ (φ \land \neg X = \emptyset) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
65	64	eqcomd	$⊢ (φ \land \neg X = \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) = A L (X) B$
66	58 65	breqtrd	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (I) \leq A L (X) B$
67	51 66	pm2.61dan	$⊢ φ \to voln* (X) (I) \leq A L (X) B$
68	49 35	eqeltrd	$⊢ (φ \land X = \emptyset) \to A L (X) B \in ℝ$
69	50	eqcomd	$⊢ (φ \land X = \emptyset) \to A L (X) B = voln* (X) (I)$
70	68 69	eqled	$⊢ (φ \land X = \emptyset) \to A L (X) B \leq voln* (X) (I)$
71		fveq1	$⊢ a = c \to a (k) = c (k)$
72	71	fvoveq1d	$⊢ a = c \to vol ([a (k), b (k))) = vol ([c (k), b (k)))$
73	72	prodeq2ad	$⊢ a = c \to \prod_{k \in x} vol ([a (k), b (k))) = \prod_{k \in x} vol ([c (k), b (k)))$
74	73	ifeq2d	$⊢ a = c \to if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), b (k))))$
75		fveq1	$⊢ b = d \to b (k) = d (k)$
76	75	oveq2d	$⊢ b = d \to [c (k), b (k)) = [c (k), d (k))$
77	76	fveq2d	$⊢ b = d \to vol ([c (k), b (k))) = vol ([c (k), d (k)))$
78	77	prodeq2ad	$⊢ b = d \to \prod_{k \in x} vol ([c (k), b (k))) = \prod_{k \in x} vol ([c (k), d (k)))$
79	78	ifeq2d	$⊢ b = d \to if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), b (k)))) = if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), d (k))))$
80	74 79	cbvmpov	$⊢ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (c \in (ℝ^{x}), d \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), d (k)))))$
81	80	a1i	$⊢ x = y \to (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (c \in (ℝ^{x}), d \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), d (k)))))$
82		oveq2	$⊢ x = y \to ℝ^{x} = ℝ^{y}$
83		eqeq1	$⊢ x = y \to (x = \emptyset \leftrightarrow y = \emptyset)$
84		prodeq1	$⊢ x = y \to \prod_{k \in x} vol ([c (k), d (k))) = \prod_{k \in y} vol ([c (k), d (k)))$
85	83 84	ifbieq2d	$⊢ x = y \to if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), d (k)))) = if (y = \emptyset, 0, \prod_{k \in y} vol ([c (k), d (k))))$
86	82 82 85	mpoeq123dv	$⊢ x = y \to (c \in (ℝ^{x}), d \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([c (k), d (k))))) = (c \in (ℝ^{y}), d \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([c (k), d (k)))))$
87	81 86	eqtrd	$⊢ x = y \to (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (c \in (ℝ^{y}), d \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([c (k), d (k)))))$
88	87	cbvmptv	$⊢ (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) = (y \in Fin ⟼ (c \in (ℝ^{y}), d \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([c (k), d (k))))))$
89	5 88	eqtri	$⊢ L = (y \in Fin ⟼ (c \in (ℝ^{y}), d \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([c (k), d (k))))))$
90		eqeq1	$⊢ w = z \to (w = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k)))) \leftrightarrow z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k)))))$
91	90	anbi2d	$⊢ w = z \to ((I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land w = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))))$
92	91	rexbidv	$⊢ w = z \to (\exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land w = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow \exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))))$
93		simpl	$⊢ (h = i \land j \in ℕ) \to h = i$
94	93	fveq1d	$⊢ (h = i \land j \in ℕ) \to h (j) = i (j)$
95	94	coeq2d	$⊢ (h = i \land j \in ℕ) \to [.) \circ h (j) = [.) \circ i (j)$
96	95	fveq1d	$⊢ (h = i \land j \in ℕ) \to ([.) \circ h (j)) (k) = ([.) \circ i (j)) (k)$
97	96	ixpeq2dv	$⊢ (h = i \land j \in ℕ) \to \underset{k \in X}{⨉} ([.) \circ h (j)) (k) = \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
98	97	iuneq2dv	$⊢ h = i \to ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
99	98	sseq2d	$⊢ h = i \to (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \leftrightarrow I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
100		simpl	$⊢ (h = i \land k \in X) \to h = i$
101	100	fveq1d	$⊢ (h = i \land k \in X) \to h (j) = i (j)$
102	101	coeq2d	$⊢ (h = i \land k \in X) \to [.) \circ h (j) = [.) \circ i (j)$
103	102	fveq1d	$⊢ (h = i \land k \in X) \to ([.) \circ h (j)) (k) = ([.) \circ i (j)) (k)$
104	103	fveq2d	$⊢ (h = i \land k \in X) \to vol (([.) \circ h (j)) (k)) = vol (([.) \circ i (j)) (k))$
105	104	prodeq2dv	$⊢ h = i \to \prod_{k \in X} vol (([.) \circ h (j)) (k)) = \prod_{k \in X} vol (([.) \circ i (j)) (k))$
106	105	mpteq2dv	$⊢ h = i \to (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
107	106	fveq2d	$⊢ h = i \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
108	107	eqeq2d	$⊢ h = i \to (z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k)))) \leftrightarrow z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
109	99 108	anbi12d	$⊢ h = i \to ((I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow (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))))))$
110	109	cbvrexvw	$⊢ \exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow \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)))))$
111	110	a1i	$⊢ w = z \to (\exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow \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))))))$
112	92 111	bitrd	$⊢ w = z \to (\exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land w = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k))))) \leftrightarrow \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))))))$
113	112	cbvrabv	$⊢ \{w \in ℝ^{} \| \exists h \in ({({ℝ^{2}}^{X})}^{ℕ}) (I \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ h (j)) (k) \land w = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ h (j)) (k)))))\} = \{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)))))\}$
114		simpl	$⊢ (j = n \land l \in X) \to j = n$
115	114	fveq2d	$⊢ (j = n \land l \in X) \to i (j) = i (n)$
116	115	fveq1d	$⊢ (j = n \land l \in X) \to i (j) (l) = i (n) (l)$
117	116	fveq2d	$⊢ (j = n \land l \in X) \to 1^{st} (i (j) (l)) = 1^{st} (i (n) (l))$
118	117	mpteq2dva	$⊢ j = n \to (l \in X ⟼ 1^{st} (i (j) (l))) = (l \in X ⟼ 1^{st} (i (n) (l)))$
119	118	cbvmptv	$⊢ (j \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (j) (l)))) = (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l))))$
120	119	mpteq2i	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (j \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (j) (l))))) = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 1^{st} (i (n) (l)))))$
121	116	fveq2d	$⊢ (j = n \land l \in X) \to 2^{nd} (i (j) (l)) = 2^{nd} (i (n) (l))$
122	121	mpteq2dva	$⊢ j = n \to (l \in X ⟼ 2^{nd} (i (j) (l))) = (l \in X ⟼ 2^{nd} (i (n) (l)))$
123	122	cbvmptv	$⊢ (j \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (j) (l)))) = (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l))))$
124	123	mpteq2i	$⊢ (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (j \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (j) (l))))) = (i \in ({({ℝ^{2}}^{X})}^{ℕ}) ⟼ (n \in ℕ ⟼ (l \in X ⟼ 2^{nd} (i (n) (l)))))$
125	59 61 62 63 4 89 113 120 124	ovnhoilem2	$⊢ (φ \land \neg X = \emptyset) \to A L (X) B \leq voln* (X) (I)$
126	70 125	pm2.61dan	$⊢ φ \to A L (X) B \leq voln* (X) (I)$
127	13 16 67 126	xrletrid	$⊢ φ \to voln* (X) (I) = A L (X) B$

Metamath Proof Explorer

Theorem ovnhoi

Proof