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	$$⊢\phi \to X\in \mathrm{Fin}$$
	ioovonmbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
	ioovonmbl.a	$$⊢\phi \to A:X⟶{ℝ}^{*}$$
	ioovonmbl.b	$$⊢\phi \to B:X⟶{ℝ}^{*}$$
Assertion	ioovonmbl	$$⊢\phi \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		ioovonmbl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ioovonmbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3		ioovonmbl.a	$$⊢\phi \to A:X⟶{ℝ}^{*}$$
4		ioovonmbl.b	$$⊢\phi \to B:X⟶{ℝ}^{*}$$
5	1 3 4	ioorrnopnxr
6	1 2 5	opnvonmbl	$$⊢\phi \to \underset{i\in X}{⨉}\left(A\left(i\right),B\left(i\right)\right)\in S$$