Theorem iccvonmbl

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	iccvonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	iccvonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	iccvonmbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	iccvonmbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
Assertion	iccvonmbl	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		iccvonmbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		iccvonmbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		iccvonmbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		iccvonmbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑖 ) )
6	5	oveq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝐴 ‘ 𝑗 ) − ( 1 / 𝑛 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) )
7	6	cbvmptv	⊢ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) − ( 1 / 𝑛 ) ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) )
8	7	mpteq2i	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑗 ) − ( 1 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 1 / 𝑛 ) ) ) )
9		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑖 ) )
10	9	oveq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝐵 ‘ 𝑗 ) + ( 1 / 𝑛 ) ) = ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) )
11	10	cbvmptv	⊢ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑗 ) + ( 1 / 𝑛 ) ) ) = ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) )
12	11	mpteq2i	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑗 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑗 ) + ( 1 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑖 ∈ 𝑋 ↦ ( ( 𝐵 ‘ 𝑖 ) + ( 1 / 𝑛 ) ) ) )
13	1 2 3 4 8 12	iccvonmbllem	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,] ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )