Theorem opnvonmbl

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	opnvonmbl.x	|- ( ph -> X e. Fin )
	opnvonmbl.s	|- S = dom ( voln ` X )
	opnvonmbl.g	|- ( ph -> G e. ( TopOpen ` ( RR^ ` X ) ) )
Assertion	opnvonmbl	|- ( ph -> G e. S )

Proof

Step	Hyp	Ref	Expression
1		opnvonmbl.x	|- ( ph -> X e. Fin )
2		opnvonmbl.s	|- S = dom ( voln ` X )
3		opnvonmbl.g	|- ( ph -> G e. ( TopOpen ` ( RR^ ` X ) ) )
4		fveq2	|- ( k = i -> ( ( [,) o. f ) ` k ) = ( ( [,) o. f ) ` i ) )
5	4	cbvixpv	|- X_ k e. X ( ( [,) o. f ) ` k ) = X_ i e. X ( ( [,) o. f ) ` i )
6	5	a1i	|- ( f = h -> X_ k e. X ( ( [,) o. f ) ` k ) = X_ i e. X ( ( [,) o. f ) ` i ) )
7		coeq2	|- ( f = h -> ( [,) o. f ) = ( [,) o. h ) )
8	7	fveq1d	|- ( f = h -> ( ( [,) o. f ) ` i ) = ( ( [,) o. h ) ` i ) )
9	8	ixpeq2dv	|- ( f = h -> X_ i e. X ( ( [,) o. f ) ` i ) = X_ i e. X ( ( [,) o. h ) ` i ) )
10	6 9	eqtrd	|- ( f = h -> X_ k e. X ( ( [,) o. f ) ` k ) = X_ i e. X ( ( [,) o. h ) ` i ) )
11	10	sseq1d	|- ( f = h -> ( X_ k e. X ( ( [,) o. f ) ` k ) C_ G <-> X_ i e. X ( ( [,) o. h ) ` i ) C_ G ) )
12	11	cbvrabv	|- { f e. ( ( QQ X. QQ ) ^m X ) | X_ k e. X ( ( [,) o. f ) ` k ) C_ G } = { h e. ( ( QQ X. QQ ) ^m X ) | X_ i e. X ( ( [,) o. h ) ` i ) C_ G }
13	1 2 3 12	opnvonmbllem2	|- ( ph -> G e. S )