iccvonmbllem

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

	Ref	Expression
Hypotheses	iccvonmbllem.x	$⊢ φ \to X \in Fin$
	iccvonmbllem.s	$⊢ S = dom voln (X)$
	iccvonmbllem.a	$⊢ φ \to A : X ⟶ ℝ$
	iccvonmbllem.b	$⊢ φ \to B : X ⟶ ℝ$
	iccvonmbllem.c	$⊢ C = (n \in ℕ ⟼ (i \in X ⟼ A (i) - (\frac{1}{n})))$
	iccvonmbllem.d	$⊢ D = (n \in ℕ ⟼ (i \in X ⟼ B (i) + (\frac{1}{n})))$
Assertion	iccvonmbllem	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)] \in S$

Proof

Step	Hyp	Ref	Expression
1		iccvonmbllem.x	$⊢ φ \to X \in Fin$
2		iccvonmbllem.s	$⊢ S = dom voln (X)$
3		iccvonmbllem.a	$⊢ φ \to A : X ⟶ ℝ$
4		iccvonmbllem.b	$⊢ φ \to B : X ⟶ ℝ$
5		iccvonmbllem.c	$⊢ C = (n \in ℕ ⟼ (i \in X ⟼ A (i) - (\frac{1}{n})))$
6		iccvonmbllem.d	$⊢ D = (n \in ℕ ⟼ (i \in X ⟼ B (i) + (\frac{1}{n})))$
7	5	a1i	$⊢ φ \to C = (n \in ℕ ⟼ (i \in X ⟼ A (i) - (\frac{1}{n})))$
8	1	adantr	$⊢ (φ \land n \in ℕ) \to X \in Fin$
9	8	mptexd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ A (i) - (\frac{1}{n})) \in V$
10	7 9	fvmpt2d	$⊢ (φ \land n \in ℕ) \to C (n) = (i \in X ⟼ A (i) - (\frac{1}{n}))$
11	3	ffvelcdmda	$⊢ (φ \land i \in X) \to A (i) \in ℝ$
12	11	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in X) \to A (i) \in ℝ$
13		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
14	13	ad2antlr	$⊢ ((φ \land n \in ℕ) \land i \in X) \to \frac{1}{n} \in ℝ$
15	12 14	resubcld	$⊢ ((φ \land n \in ℕ) \land i \in X) \to A (i) - (\frac{1}{n}) \in ℝ$
16	10 15	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land i \in X) \to C (n) (i) = A (i) - (\frac{1}{n})$
17	16	an32s	$⊢ ((φ \land i \in X) \land n \in ℕ) \to C (n) (i) = A (i) - (\frac{1}{n})$
18	6	a1i	$⊢ φ \to D = (n \in ℕ ⟼ (i \in X ⟼ B (i) + (\frac{1}{n})))$
19	8	mptexd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ B (i) + (\frac{1}{n})) \in V$
20	18 19	fvmpt2d	$⊢ (φ \land n \in ℕ) \to D (n) = (i \in X ⟼ B (i) + (\frac{1}{n}))$
21	4	ffvelcdmda	$⊢ (φ \land i \in X) \to B (i) \in ℝ$
22	21	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in X) \to B (i) \in ℝ$
23	22 14	readdcld	$⊢ ((φ \land n \in ℕ) \land i \in X) \to B (i) + (\frac{1}{n}) \in ℝ$
24	20 23	fvmpt2d	$⊢ ((φ \land n \in ℕ) \land i \in X) \to D (n) (i) = B (i) + (\frac{1}{n})$
25	24	an32s	$⊢ ((φ \land i \in X) \land n \in ℕ) \to D (n) (i) = B (i) + (\frac{1}{n})$
26	17 25	oveq12d	$⊢ ((φ \land i \in X) \land n \in ℕ) \to (C (n) (i), D (n) (i)) = (A (i) - (\frac{1}{n}), B (i) + (\frac{1}{n}))$
27	26	iineq2dv	$⊢ (φ \land i \in X) \to ⋂_{n \in ℕ} (C (n) (i), D (n) (i)) = ⋂_{n \in ℕ} (A (i) - (\frac{1}{n}), B (i) + (\frac{1}{n}))$
28	11 21	iooiinicc	$⊢ (φ \land i \in X) \to ⋂_{n \in ℕ} (A (i) - (\frac{1}{n}), B (i) + (\frac{1}{n})) = [A (i), B (i)]$
29	27 28	eqtrd	$⊢ (φ \land i \in X) \to ⋂_{n \in ℕ} (C (n) (i), D (n) (i)) = [A (i), B (i)]$
30	29	ixpeq2dva	$⊢ φ \to \underset{i \in X}{⨉} ⋂_{n \in ℕ} (C (n) (i), D (n) (i)) = \underset{i \in X}{⨉} [A (i), B (i)]$
31	30	eqcomd	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)] = \underset{i \in X}{⨉} ⋂_{n \in ℕ} (C (n) (i), D (n) (i))$
32		eqidd	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)] = \underset{i \in X}{⨉} [A (i), B (i)]$
33		nnn0	$⊢ ℕ \neq \emptyset$
34	33	a1i	$⊢ φ \to ℕ \neq \emptyset$
35		ixpiin	$⊢ ℕ \neq \emptyset \to \underset{i \in X}{⨉} ⋂_{n \in ℕ} (C (n) (i), D (n) (i)) = ⋂_{n \in ℕ} \underset{i \in X}{⨉} (C (n) (i), D (n) (i))$
36	34 35	syl	$⊢ φ \to \underset{i \in X}{⨉} ⋂_{n \in ℕ} (C (n) (i), D (n) (i)) = ⋂_{n \in ℕ} \underset{i \in X}{⨉} (C (n) (i), D (n) (i))$
37	31 32 36	3eqtr3d	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)] = ⋂_{n \in ℕ} \underset{i \in X}{⨉} (C (n) (i), D (n) (i))$
38	1 2	dmovnsal	$⊢ φ \to S \in SAlg$
39		nnct	$⊢ ℕ ≼ ω$
40	39	a1i	$⊢ φ \to ℕ ≼ ω$
41	15	fmpttd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ A (i) - (\frac{1}{n})) : X ⟶ ℝ$
42		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
43	42	a1i	$⊢ (φ \land n \in ℕ) \to ℝ \subseteq ℝ^{*}$
44	41 43	fssd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ A (i) - (\frac{1}{n})) : X ⟶ ℝ^{*}$
45	10	feq1d	$⊢ (φ \land n \in ℕ) \to (C (n) : X ⟶ ℝ^{} \leftrightarrow (i \in X ⟼ A (i) - (\frac{1}{n})) : X ⟶ ℝ^{})$
46	44 45	mpbird	$⊢ (φ \land n \in ℕ) \to C (n) : X ⟶ ℝ^{*}$
47	23	fmpttd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ B (i) + (\frac{1}{n})) : X ⟶ ℝ$
48	47 43	fssd	$⊢ (φ \land n \in ℕ) \to (i \in X ⟼ B (i) + (\frac{1}{n})) : X ⟶ ℝ^{*}$
49	20	feq1d	$⊢ (φ \land n \in ℕ) \to (D (n) : X ⟶ ℝ^{} \leftrightarrow (i \in X ⟼ B (i) + (\frac{1}{n})) : X ⟶ ℝ^{})$
50	48 49	mpbird	$⊢ (φ \land n \in ℕ) \to D (n) : X ⟶ ℝ^{*}$
51	8 2 46 50	ioovonmbl	$⊢ (φ \land n \in ℕ) \to \underset{i \in X}{⨉} (C (n) (i), D (n) (i)) \in S$
52	38 40 34 51	saliincl	$⊢ φ \to ⋂_{n \in ℕ} \underset{i \in X}{⨉} (C (n) (i), D (n) (i)) \in S$
53	37 52	eqeltrd	$⊢ φ \to \underset{i \in X}{⨉} [A (i), B (i)] \in S$

Metamath Proof Explorer

Theorem iccvonmbllem

Proof