Theorem ioovonmbl

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

	Ref	Expression
Hypotheses	ioovonmbl.x	|- ( ph -> X e. Fin )
	ioovonmbl.s	|- S = dom ( voln ` X )
	ioovonmbl.a	|- ( ph -> A : X --> RR* )
	ioovonmbl.b	|- ( ph -> B : X --> RR* )
Assertion	ioovonmbl	|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		ioovonmbl.x	|- ( ph -> X e. Fin )
2		ioovonmbl.s	|- S = dom ( voln ` X )
3		ioovonmbl.a	|- ( ph -> A : X --> RR* )
4		ioovonmbl.b	|- ( ph -> B : X --> RR* )
5	1 3 4	ioorrnopnxr	|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. ( TopOpen ` ( RR^ ` X ) ) )
6	1 2 5	opnvonmbl	|- ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) e. S )