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	|- ( ph -> X e. Fin )
	iccvonmbl.s	|- S = dom ( voln ` X )
	iccvonmbl.a	|- ( ph -> A : X --> RR )
	iccvonmbl.b	|- ( ph -> B : X --> RR )
Assertion	iccvonmbl	|- ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		iccvonmbl.x	|- ( ph -> X e. Fin )
2		iccvonmbl.s	|- S = dom ( voln ` X )
3		iccvonmbl.a	|- ( ph -> A : X --> RR )
4		iccvonmbl.b	|- ( ph -> B : X --> RR )
5		fveq2	|- ( j = i -> ( A ` j ) = ( A ` i ) )
6	5	oveq1d	|- ( j = i -> ( ( A ` j ) - ( 1 / n ) ) = ( ( A ` i ) - ( 1 / n ) ) )
7	6	cbvmptv	|- ( j e. X |-> ( ( A ` j ) - ( 1 / n ) ) ) = ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) )
8	7	mpteq2i	|- ( n e. NN |-> ( j e. X |-> ( ( A ` j ) - ( 1 / n ) ) ) ) = ( n e. NN |-> ( i e. X |-> ( ( A ` i ) - ( 1 / n ) ) ) )
9		fveq2	|- ( j = i -> ( B ` j ) = ( B ` i ) )
10	9	oveq1d	|- ( j = i -> ( ( B ` j ) + ( 1 / n ) ) = ( ( B ` i ) + ( 1 / n ) ) )
11	10	cbvmptv	|- ( j e. X |-> ( ( B ` j ) + ( 1 / n ) ) ) = ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) )
12	11	mpteq2i	|- ( n e. NN |-> ( j e. X |-> ( ( B ` j ) + ( 1 / n ) ) ) ) = ( n e. NN |-> ( i e. X |-> ( ( B ` i ) + ( 1 / n ) ) ) )
13	1 2 3 4 8 12	iccvonmbllem	|- ( ph -> X_ i e. X ( ( A ` i ) [,] ( B ` i ) ) e. S )