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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	iccvonmbllem.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	iccvonmbllem.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	iccvonmbllem.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
	iccvonmbllem.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) )
	iccvonmbllem.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
Assertion	iccvonmbllem	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		iccvonmbllem.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		iccvonmbllem.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		iccvonmbllem.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		iccvonmbllem.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5		iccvonmbllem.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) )
6		iccvonmbllem.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
7	5	a1i	⊢ ( 𝜑 → 𝐶 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin )
9	8	mptexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) ∈ V )
10	7 9	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) )
11	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
12	11	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
13		nnrecre	⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
14	13	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
15	12 14	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ∈ ℝ )
16	10 15	fvmpt2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) = ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) )
17	16	an32s	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) = ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) )
18	6	a1i	⊢ ( 𝜑 → 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) ) )
19	8	mptexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) ∈ V )
20	18 19	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
21	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
22	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
23	22 14	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
24	20 23	fvmpt2d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) = ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) )
25	24	an32s	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) = ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) )
26	17 25	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = ( ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) (,) ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
27	26	iineq2dv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = ∩ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) (,) ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
28	11 21	iooiinicc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ∩ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) (,) ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) = ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) )
29	27 28	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) )
30	29	ixpeq2dva	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) )
31	30	eqcomd	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) = X 𝑖 ∈ 𝑋 ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) )
32		eqidd	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) = X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) )
33		nnn0	⊢ ℕ ≠ ∅
34	33	a1i	⊢ ( 𝜑 → ℕ ≠ ∅ )
35		ixpiin	⊢ ( ℕ ≠ ∅ → X 𝑖 ∈ 𝑋 ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = ∩ 𝑛 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) )
36	34 35	syl	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ∩ 𝑛 ∈ ℕ ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) = ∩ 𝑛 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) )
37	31 32 36	3eqtr3d	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑛 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) )
38	1 2	dmovnsal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
39		nnct	⊢ ℕ ≼ ω
40	39	a1i	⊢ ( 𝜑 → ℕ ≼ ω )
41	15	fmpttd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ )
42		ressxr	⊢ ℝ ⊆ ℝ^*
43	42	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ℝ ⊆ ℝ^* )
44	41 43	fssd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ^* )
45	10	feq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑛 ) : 𝑋 ⟶ ℝ^* ↔ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ^* ) )
46	44 45	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ‘ 𝑛 ) : 𝑋 ⟶ ℝ^* )
47	23	fmpttd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ )
48	47 43	fssd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ^* )
49	20	feq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ 𝑛 ) : 𝑋 ⟶ ℝ^* ↔ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) : 𝑋 ⟶ ℝ^* ) )
50	48 49	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) : 𝑋 ⟶ ℝ^* )
51	8 2 46 50	ioovonmbl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑖 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ 𝑆 )
52	38 40 34 51	saliincl	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ X 𝑖 ∈ 𝑋 ( ( ( 𝐶 ‘ 𝑛 ) ‘ 𝑖 ) (,) ( ( 𝐷 ‘ 𝑛 ) ‘ 𝑖 ) ) ∈ 𝑆 )
53	37 52	eqeltrd	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Metamath Proof Explorer

Theorem iccvonmbllem

Proof